论文部分内容阅读
提出采用模型检验方法研究电子商务协议的非否认性与公平性问题,建立了认证电子邮件协议CMP1的有限状态机模型,并用SMV检验工具对其非否认性与公平性进行了分析检验,经过分析发现了CMP1协议不满足公平性并对其进行了相应修改.结果表明,利用符号模型检验方法分析检验电子商务协议的新特性是行之有效的.
CMP1协议的符号模型检验分析
【摘 要】
：
提出采用模型检验方法研究电子商务协议的非否认性与公平性问题,建立了认证电子邮件协议CMP1的有限状态机模型,并用SMV检验工具对其非否认性与公平性进行了分析检验,经过分析
【机 构】
：
贵州财经学院,贵州财经学院,贵州大学
【出 处】
：
海军工程大学学报
【发表日期】
：
2005年3期
其他文献
“徐研1号”是江苏省徐州市蔬菜研究所选育的辣椒品种，生长势强，叶色深绿，株高69厘米，开展度80厘米．始花节位在9—10节．连续结果能力强，果实膨大速度快。果实长灯笼形．绿色，果长约9．6厘
在经济社会高度发达的今天,航空业获得迅猛的发展,如通用航空区域的发展,航空运输业的发展等构成了新的经济增长点,加快了物质运转的速度,促进了经济的发展,同时民用航空也为
乌申斯基说过：“没有兴趣的强制性学习，将会扼杀学生探求真理的欲望。”在数学教学中，我们可以利用各种教学手段来刺激学生的感官，丰富学生的感性认识，使学生始终保持浓厚的学习兴趣和积极的情感，主动参与教学中的思维活动，变“要我学”为“我要学”。 一、在导入中掀高潮 在课堂教学的起始环节，教师要通过创设情境、组织游戏、设置疑问、讲故事等多种有趣的形式，吸引学生的注意力，激发学生的求知欲，用最短的时间进
《国家体育总局规章和规范性文件制定程序规定》已于2017年12月1日经国家体育总局第19次局长办公会审议通过，现予公布，自2018年1月1日起施行。局长苟仲文2017年12月6日
学生在解答应用题时，有时会遇到看上去比较难、比较繁的题目，其实这些应用题中隐含着特殊条件，在解题时如能抓住这些特殊条件，找准隐含关系，可以解得更巧妙、更简单。 “注：本文中所涉及到的图表、注解、公式等内容请以PDF格式阅读原文”。 本文为全文原貌 未安
被污染液压油的加热过滤装置李俊红刘秋来（山西长治液压件厂）当前，随着液压件产量不断增加，产品试验中使用的工作介质——液压油的消耗量也不断增加。由于污染度超差，液压油不能继
城市变化监控能够有效帮助政府机关和城区规划部门更新地图并制定长远的发展计划。论文提出了一个基于 Log-Gabor 滤波器快速提取遥感图像中居民区域的新方法。方法分为三步：
针对某高性能水泥分解炉的实际尺寸,分别采用Eulerian模型、mixture模型和离散相模型模拟了炉内气固两相三维流场,结果显示Eulerian (mixture)模型模拟所得炉内速度、压力、
1．选用良种。宜选用品质好、适应性强、抗病、丰产品种，如红皮南瓜早生赤栗、绿皮南瓜北京甜栗等。其共同特点是：早熟，生长势强，耐白粉病，连续结果性好，果实外形整齐美观，果肉橘黄，肉