摘要
如何融合计算密码学与形式演算模型两条途径以有效分析和证明复杂密码协议,是信息安全领域富有挑战性的问题之一.文中提出Dolev-Yao刚性和Dolev-Yao相似性概念,运用密码协议的语法骨架提取与语义赋值技术,建立起一个能涵盖除具有适应性入侵能力之外的任何主动攻击者和大部分有实际意义的非自由消息代数的理论分析框架.该框架内所证明的协议安全性质具有复合-稳定性,即所证明的安全性质在协议与环境复合时仍然保持成立.文中针对strand-图模型这一具体情形证明了Canetti的UC-相似性概念与这里所建立的Dolev-Yao相似性概念之间接近充分必要程度的对偶关系,从而对融合UC-理论/strand-图模型这一情形具体证明了该分析框架具有相容性和完备性.最后,根据以上理论结果讨论了如何建立一种对应的新的协议分析方法.
How to integrate computational and symbolic approaches to analyzing complicated cryptographic protocols is one of the most challenging problems in information security area. In this paper the authors propose a novel theoretical framework to analyze cryptographic protocols covering almost all real-world non-flee message algebras and against non-adaptive malicious adversaries, based-upon two novel concepts of "Dolev-Yao nonmalleability" and "Dolev-Yao emulation", techniques of symbolic extraction and semantic assignment. Security properties proved in this framework are universally composable, i. e. , all security properties are provably-preserved when combined with any running environment. The authors prove that Canetti's concept of UC emulation and the concept of Dolev-Yao emulation are almost sufficient-and-necessarily dual each other with respect to integrating UC theory and strand symbolic model(Dolev-Yao style), and this analysis framework is proven both sound and complete in this case. In addition, a new method for cryptographic protocol analysis is established based-on the above theoretical consequences.
出处
《计算机学报》
EI
CSCD
北大核心
2009年第4期618-634,共17页
Chinese Journal of Computers
基金
国家自然科学基金(60673046)
辽宁省自然科学基金(2075068)
大连理工大学跨学科建设项目资助