基于CPN模型的不可否认协议分析  

Formal Analysis of Non-Repudiation Protocol based on Colored Petri Net Model

作　　者：苏桂平[1] 孙莎[2] 

机构地区：[1]中国科学院研究生院信息科学与工程学院,北京100049 [2]中国科学院研究生院工程教育学院,北京100049

出　　处：《信息安全与通信保密》2011年第8期54-55,58,共3页Information Security and Communications Privacy

摘　　要：通过对不可否认协议的语义进行分析,建立有色Petri网(Coloured Petri Net,CPN)中基本元素与安全协议中元素的对应关系,对CPN Tools提供的建模语言(CPN ML)在规范协议描述、简化协议建模及自动检测方面进行扩展,提出了一种基于CPN模型的不可否认协议分析方法,该方法利用CPN tools的状态空间查询功能和自建的查询函数库来对不可否认协议进行分析和验证,该工具具有通用性强、时效性强和交互性好等诸多优点,并通过实例说明了这种方法的有效性。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.

关 键 词：不可否认协议 有色Petri模型 形式化分析 

分 类 号：TN918.91[电子电信—通信与信息系统]