【摘要】 从目前的研究成果来看,基于CPN(Colored Petri Nets,着色Petri网)的密码协议形式化建模及其分析方法主要采用传统的Dolev-Yao攻击者模型。针对该攻击者模型在验证协议中存在的不足,提出一种改进的基于CPN的攻击者模型,利用该模型对具体的NS协议进行建模和分析,实验证明,对模型的改进完善了基于CPN的密码协议形式化建模和分析方法。更多还原

【Abstract】 According to the results of the current study,formal modeling and analysis of Cryptographic Protocols Using Colored Petri Nets is mainly based on traditional Dolev- Yao attacker model. Since the attacker model used in protocol verification is nor perfect,an improved attacker model based on CPN model is proposed. Then it is used to the NSL protocol by modeling and analyzing. The experiment proves the improvement of formal modeling of cryptographic protocol using CPN.更多还原