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

Analysis and Performance Evaluation of Cryptographic Protocol Using Timed Petri Net

作　　者：张广胜[1] 

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

出　　处：《计算机工程与应用》2003年第30期158-161,共4页Computer Engineering and Applications

基　　金：国家自然科学基金资助课题(编号:60173053)

摘　　要：形式化分析方法由于其精炼、简洁和无二义性逐步成为分析密码协议的一条可靠和准确的途径,但是密码协议的形式化分析研究目前还不够深入,针对这一现状,该文提出用时延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.

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

分 类 号：TP393[自动化与计算机技术—计算机应用技术]