基于时延Petri网的密码协议分析及性能评估

Analysis and Performance Evaluation of Cryptographic Protocol Using Timed Petri Net

形式化分析方法由于其精炼、简洁和无二义性逐步成为分析密码协议的一条可靠和准确的途径,但是密码协议的形式化分析研究目前还不够深入,针对这一现状,该文提出用时延Petri网来表示和分析密码协议。该模型不但能够反映协议的静态和动态的特性,而且能够对密码协议进行时间、空间上的性能评估。作为实例,文章对MSR无线协议作了详细的形式分析和性能评估。最后,与其它形式化分析密码协议的方法作了比较。

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 method not only specifies the static and dynamic properties but al-so evaluates the performance of cryptographic protocol(mainly time delay and software complexity).Applying this method to the MSR wireless protocol,this paper verifies the known attacks on it and points out several attacking scenarios.Comparing with relevant ones,it is a better formal way to represent cryptographic protocol.