Chinese Journal of Computers   Full Text
Title	Cryptographic Protocol Analysis
Authors	TIAN Yuan1) WANG Ying2) JIN Feng1) JIN Yue1)
Address	1)(Software School of Dalian University of Technology, Dalian, Liaoning 116620) 2)(School of Mathematical Science, Dalian Unversity of Technology, Dalian, Liaoning 116620)
Year	2009
Issue	No.4(618—634)
Abstract &   Background	Abstract 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-free 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. Keywords computational cryptography; symbolic model; UC emulation; Dolev-Yao non-malleability; Dolev-Yao emulation Background How to integrate computational and symbolic approaches to analyzing complicated cryptographic protocols is one of the most challenging problems in information security area, however, almost none existed approach can reach satisfactory composability in real-world aspects. Based-upon two novel concepts of “Dolev-Yao nonmalleability” and “Dolev-Yao emulation”, our approach establishes an analysis framework covering real-world non-free message algebras and against malicious adversaries via 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 malicious runtime environment. One of the novelties in this approach is that Canetti’s concept of UC emulation and our concept of Dolev-Yao emulation are dual each other and this analysis framework is both sound and complete. Based-on the above theoretical consequences, a new method for cryptographic protocol analysis is under systematic construction in the project supported by Chinese NFS which ultimate objective is to develop new efficient techniques to implement the automated system for semantic verification of cryptographic protocols. More Concretely, this research systematically applies this method to integrate computational setting and symbolic setting of strand model, process algebra model and process calculus model respectively, develops efficient analysis algorithms and automated verification tools and applies these tools to real-world cryptographic protocols design and analysis. The consequences in this paper contributes theoretical foundations and elementary techniques to this research.