| 基于CPN模型的不可否认协议分析 |
| |
| 引用本文： | 苏桂平,孙莎. 基于CPN模型的不可否认协议分析[J]. 信息安全与通信保密, 2011, 9(8): 54-55,58 |
| |
| 作者姓名： | 苏桂平 孙莎 |
| |
| 作者单位： | 1. 中国科学院研究生院信息科学与工程学院,北京,100049
2. 中国科学院研究生院工程教育学院,北京,100049 |
| |
| 摘 要： | 通过对不可否认协议的语义进行分析,建立有色Petri网（Coloured Petri Net,CPN）中基本元素与安全协议中元素的对应关系,对CPN Tools提供的建模语言（CPN ML）在规范协议描述、简化协议建模及自动检测方面进行扩展,提出了一种基于CPN模型的不可否认协议分析方法,该方法利用CPN tools的状态空间查询功能和自建的查询函数库来对不可否认协议进行分析和验证,该工具具有通用性强、时效性强和交互性好等诸多优点,并通过实例说明了这种方法的有效性。
|
| 关 键 词： | 不可否认协议 有色Petri模型 形式化分析 |
Formal Analysis of Non-Repudiation Protocol based on Colored Petri Net Model |
| |
| SU Gui-ping,SUN Sha. Formal Analysis of Non-Repudiation Protocol based on Colored Petri Net Model[J]. China Information Security, 2011, 9(8): 54-55,58 |
| |
| Authors: | SU Gui-ping SUN Sha |
| |
| Affiliation: | SU Gui-ping1,SUN Sha2(1School of Information Science and Engineering,Graduate School of CAS,Beijing 100049,China,2College of Engineering and Education,China) |
| |
| Abstract: | The semantics of non-repudiation protocol is analyzed,and the corresponding relation of between the basic elements of CPN and the elements of security agreement established.The modeling language（CPN ML） provided by CPN Tools is extended,thus a CPN model-based non-repudiation protocol Analysis method is proposed.Examples and experiment verify the effectiveness of this method. |
| |
| Keywords: | non-repudiation protocol coloured petri model formal analysis |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
