|
|||||
|
|
| CMP1协议的符号模型检验分析 | |
| 引用本文： | 张梅,文静华,杨滋荣,李祥.CMP1协议的符号模型检验分析[J].海军工程大学学报,2005,17(3):15-18. |
| 作者姓名： | 张梅 文静华 杨滋荣 李祥 |
| 作者单位： | 1. 贵州财经学院,信息学院,贵州,贵阳,550004 2. 贵州财经学院,信息学院,贵州,贵阳,550004;贵州大学,计算机软件与理论研究所,贵州,贵阳,550025 3. 贵州大学,计算机软件与理论研究所,贵州,贵阳,550025 |
| 基金项目： | 国家自然科学基金资助项目(10161005)，贵州省自然科学基金资助项目(20043029)，贵州省教育厅自然科学基金资助项目 |
| 摘 要： | 提出采用模型检验方法研究电子商务协议的非否认性与公平性问题,建立了认证电子邮件协议CMP1的有限状态机模型,并用SMV检验工具对其非否认性与公平性进行了分析检验,经过分析发现了CMP1协议不满足公平性并对其进行了相应修改.结果表明,利用符号模型检验方法分析检验电子商务协议的新特性是行之有效的. |
| 关 键 词： | 电子商务协议 公平性 符号模型检测 |
| 文章编号： | 1009-3486(2005)03-0015-04 |
| 修稿时间： | 2005年1月16日 |
Symbolic model checking analysis for CMP1 protocol |
|
| ZHANG Mei,WEN Jing-hua,Yang Zi-rong,LI Xiang.Symbolic model checking analysis for CMP1 protocol[J].Journal of Naval University of Engineering,2005,17(3):15-18. | |
| Authors: | ZHANG Mei WEN Jing-hua Yang Zi-rong LI Xiang |
| Abstract: | A new approach is proposed for analyzingthe non-repudiation and fairnessproperty of E-commerce protocols. The authentication E-mail protocol CMP1 is modeled as finite state machine, and their two vital aspects of non-repudiationpropertyand fairness propertyare analyzed byusing SMV. It is found that the fairness property can not be satisfied, and thus some corrections are made on the finite state machine of CMP1 protocols. This result shows that it is effective to analyze and check the new property of E-commerce protocolsby the symbolmodel checker. |
| Keywords: | E-commerce protocols fairness symbolic model checking |
| 本文献已被 CNKI 万方数据 等数据库收录！ | |