基于时间Petri网的密码协议分析  

Analysis Cryptographic Protocol Using Timed Petri Net

作　　者：张广胜[1] 吴哲辉[1] 逄玉叶 

机构地区：[1]山东科技大学信息学院,山东泰安271019 [2]山东大学信息科学与工程学院,山东济南250100

出　　处：《系统仿真学报》2003年第z1期11-16,共6页Journal of System Simulation

基　　金：国家自然科学基金资助项目(60173053)

摘　　要：形式化分析方法由于其精炼、简洁和无二义性逐步成为分析密码协议的一条可靠和准确的途径,但是密码协议的形式化分析研究目前还不够深入。在文中首先对四类常见的密码协议形式化分析方法作了一些比较,阐述了各自的特点,然后用时间Petri网来表示和分析密码协议。该方法不但能够反映协议的静态和动态的特性,而且能够对密码协议进行时间、空间上的性能评估。作为实例,对Aziz-Diffie 无线协议作了详细的形式分析和性能评估,验证了已知的、存在的漏洞,并且给出了该协议的改进方案。The paper analysis four kinds of formal methods for the analysis of cryptographic protocol and set forth the merits and disadvantages of each. In order to develop a unified theory to verify cryptographic protocol, this paper provides a way to describe cryptographic protocol based on timed Petri net. This methods not only specifies the static and dynamic properties but also evaluates the performance of cryptographic protocol (mainly time delay and software complexity). Applying this method to the wireless protocol proposed by Aziz and Diffie, this paper verifies the known attacks on it and points out several attacking scenarios. Finally, An improvement on Aziz-Diffle protocol is proposed.

关 键 词：密码协议 形式化分析 时间PETRI网 BAN逻辑 认证协议 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]