改进身份认证协议的形式化描述与验证

作     者：梁爽 吴晓艳 王怀江 LIANG Shuang;WU Xiao-yan;WANG Huai-jiang

作者机构：沈阳理工大学应用技术学院辽宁抚顺113122 沈阳铁路信号工厂开发部辽宁沈阳110025 

出 版 物：《计算机工程与设计》 (Computer Engineering and Design)

年 卷 期：2009年第30卷第13期

页      码：3075-3077页

摘      要：以前用着色Petri网验证协议,大多只验证了其正确性,采用着色Petri网对自行设计的基于PKI的动态身份认证系统的安全性进行了描述和验证;一般在使用传统1-可达性分析方法分析复杂身份认证协议时,会存在状态空间爆炸的问题。为了有效地解决该问题,提出了一种用1-可达性分析方法和向回分析方法相结合的策略,对该身份认证协议进行了分析,从而验证了该身份认证协议是安全的。

主 题 词：身份认证协议 Petri网 可达树 可达性分析 安全性 形式化描述 

学科分类：08[工学] 0839[0839] 081201[081201] 0812[工学-测绘类] 

D　O　I：10.16208/j.issn1000-7024.2009.13.047

馆 藏 号：203517890...