摘要
以前用着色Petri网验证协议,大多只验证了其正确性,采用着色Petri网对自行设计的基于PKI的动态身份认证系统的安全性进行了描述和验证;一般在使用传统1-可达性分析方法分析复杂身份认证协议时,会存在状态空间爆炸的问题。为了有效地解决该问题,提出了一种用1-可达性分析方法和向回分析方法相结合的策略,对该身份认证协议进行了分析,从而验证了该身份认证协议是安全的。
Colored Petri net used to verify the agreement, most of them only to verify its correctness, the self designed security ot FKI- based authentication system is described and validated.There are the problem of state space explosion when analyze the complexity authentication protocol by the traditional 1- reachability analysis method. In order to effectively solve the problem, a measure is put forward which is combining the 1- teachability analysis method and the backward analysis method. This paper has adopt the measure to analyze the PKI-based authentication protocol, so the security of the protocol is verified.
出处
《计算机工程与设计》
CSCD
北大核心
2009年第13期3075-3077,共3页
Computer Engineering and Design
