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

形式化分析方法由于其精炼、简洁和无二义性逐步成为分析密码协议的一条可靠和准确的途径,但是密码协议的形式化分析研究目前还不够深入.在文中首先对四类常见的密码协议形式化分析方法作了一些比较,阐述了各自的特点,然后用时间Petri网来表示和分析密码协议.该方法不但能够反映协议的静态和动态的特性,而且能够对密码协议进行时间、空间上的性能评估.作为实例,对Aziz-Diffie无线协议作了详细的形式分析和性能评估,验证了已知的、存在的漏洞,并且给出了该协议的改进方案.

Analysis Cryptographic Protocol Using Timed Petri Net

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.