归约方法与形式化方法相结合的安全协议验证技术研究

面向各种实用的安全协议，提出层次化、组合化的基于归约方法与形式化方法相结合的安全协议验证技术和算法，并建立相应的计算机辅助工具．主要内容包括：（１）研究高效的安全性归约方法；（２）研究利用形式化方法使得归约方法自动化或半自动化；（３）研究利用归约方法说明形式化公理与定理在计算安全意义下的合理性与完备性；（4）结合归约方法和形式化方法设计各种能够普遍组合的可证明安全协议；（5）与此相关的概率逻辑分析