论文部分内容阅读
以基于四方的安全电子商务支付协议为研究对象,建立了协议的有限状态模型以及安全计算树逻辑CTL公式,利用符号模型检测工具SMV对协议的原子性进行检测验证。验证结果证明,基于四方的安全电子商务支付协议满足电子支付的金钱原子性、商品原子性以及确认发送原子性,协议符合电子支付的原子性安全要求。
基于四方的安全电子商务支付协议分析与验证
【摘 要】
：
以基于四方的安全电子商务支付协议为研究对象,建立了协议的有限状态模型以及安全计算树逻辑CTL公式,利用符号模型检测工具SMV对协议的原子性进行检测验证。验证结果证明,基
【机 构】
：
华中科技大学计算机学院
【出 处】
：
计算机科学
【发表日期】
：
2012年03期
【基金项目】
：
国家自然科学基金(70672041);湖北省自然科学基金(2007ABA307);中央高校基本科研业务费(2010MS112)资助
其他文献
理论对实践有着重要的指导意义,管理理论对大学生管理更是有着非常重要的意义。本文从管理理论出发,本文通过分析大学生的管理现状,由表及里,探索更加有效的大学生管理策略,
在《儿子与情人》中,英国作家戴·赫·劳伦斯以英国诺丁汉郡矿工的生活为背景,描写了莫雷尔一家的感情纠葛与冲突,反映了资本主义工业文明在发展过程中所产生的种种矛盾和问
光助类芬顿反应相对于传统的均相Fenton法,具有可减少铁离子的二次污染、催化剂容易回收再利用、提高催化能力和有效利用太阳能等显著特点而备受重视,但光助类芬顿催化剂的稳
医疗纠纷行政调解作为一种诉讼外纠纷解决方式应当遵循自愿原则、效率原则和合法原则。在具体制度设计上可以考虑在县级以上地方政府法制部门成立相对独立的机构负责医疗纠纷
<正>1吸入麻醉药和仪器的准备1.1药物1.1.1氧化亚氮(笑气)有钢瓶装和管道供气两种形式(1)钢瓶装氧化亚氮的压力为745psi(52kg/cm2),到麻醉机压力降低至45psi(约3kg/cm2)(2)管
目的建立一种简便高效的海马神经元的原代培养方法。方法无菌环境下取新生SD大鼠(24 h内)海马,清洗、剪碎,以0.25%胰蛋白酶消化,200目滤网过滤,混合培养,约5 d后加入阿糖胞苷
为研究锈胀对钢筋混凝土梁疲劳性能的影响,采用电化学快速锈蚀试验得到了不同锈胀程度的钢筋混凝土梁,讨论了初始锈胀裂缝的宽度及分布情况。开展了钢筋混凝土梁的静力及疲劳
目的探讨白藜芦醇(Res)对去卵巢(OVX)大鼠空间记忆及突触可塑性的影响。方法将成年雌性SD大鼠40只随机分为OVX组、Res 80 mg/kg组、雌二醇替代组(ERT)和假手术组。大鼠除去卵
<正>又是一年春草绿,又是清明寒食时!在这草长莺飞的阳春三月,我们怀着愉悦的心情迎接新生命的到来,期待春暖花开、万物复苏的繁华季节。与此同时,第三届清明寒食文化节也如
会议