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

摘要

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