论文部分内容阅读
如何融合计算密码学与形式演算模型两条途径以有效分析和证明复杂密码协议,是信息安全领域富有挑战性的问题之一.文中提出Dolev-Yao刚性和Dolev-Yao相似性概念,运用密码协议的语法骨架提取与语义赋值技术,建立起一个能涵盖除具有适应性入侵能力之外的任何主动攻击者和大部分有实际意义的非自由消息代数的理论分析框架.该框架内所证明的协议安全性质具有复合-稳定性,即所证明的安全性质在协议与环境复合时仍然保持成立.文中针对strand-图模型这一具体情形证明了Canetti的UC-相似性概念与这里所建立的Dol