作者：梁爽 吴晓艳 王怀江身份认证协议petri网可达树可达性分析安全性形式化描述
摘要：以前用着色Petri网验证协议,大多只验证了其正确性,采用着色Petri网对自行设计的基于PKI的动态身份认证系统的安全性进行了描述和验证;一般在使用传统1-可达性分析方法分析复杂身份认证协议时,会存在状态空间爆炸的问题。为了有效地解决该问题,提出了一种用1-可达性分析方法和向回分析方法相结合的策略,对该身份认证协议进行了分析,从而验证了该身份认证协议是安全的。
注：因版权方要求，不能公开全文，如需全文，请咨询杂志社
