一种安全协议的形式化设计方法

本文以协议分析器为辅助工具，结合定理证明方法，给出一个安全协议形式化设计方法。该方法首先根据协议规范构造全信息项及冗余协议，使用定理证明保证冗余协议的安全性。对冗余协议利用安全性保持约简规则和随机约简规则进行约简，从而得到最优约简协议。该方法实现了安全协议的自动设计，具有良好的扩展性，可以根据需求和协议的发展增加设计规则和约简规则。

A Formal Method of Security Protocol Design

This paper proposes a new method of security protocol design using theorem proven and security protocol analyzer.It constructs full information items based on requirement to get a redundancy protocol firstly,and then uses theorem proven to prove the security of the designed protocol.lt reduces the redundancy protocol step by step,using the reduction rules supported by theorem proven,until it gets optimized protocols which meet the requirement of protocol, The method can realize auto-design of security protocol and has good extension for design rules and reduction rules.