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