|
|||||
|
|
| 改进身份认证协议的形式化描述与验证 | |
| 引用本文： | 梁爽,吴晓艳,王怀江.改进身份认证协议的形式化描述与验证[J].计算机工程与设计,2009,30(13). |
| 作者姓名： | 梁爽 吴晓艳 王怀江 |
| 作者单位： | 1. 沈阳理工大学,应用技术学院,辽宁,抚顺,113122 2. 沈阳铁路信号工厂,开发部,辽宁,沈阳,110025 |
| 摘 要： | 以前用着色Petri网验证协议,大多只验证了其正确性,采用着色Petri网对自行设计的基于PKI的动态身份认证系统的安全性进行了描述和验证;一般在使用传统1-可达性分析方法分析复杂身份认证协议时,会存在状态空间爆炸的问题,为了有效地解决该问题,提出了一种用1-可迭性分析方法和向回分析方法相结合的策略,对该身份认证协议进行了分析,从而验证了该身份认证协议是安全的. |
| 关 键 词： | 身份认证协议 Petri网 可迭树 可达性分析 安全性 形式化描述 |
| 本文献已被 万方数据 等数据库收录！ | |