Analyzing NSPK with the Applied Pi Calculus
We present a framework for describing and analyzing cryptography protocols based on the Applied Pi calculus. The Needham-Schroeder Publick Key protocol (NSPK for short) and its fixed version by Lowe are modelled in this framework. Authentication is analyzed with the bisimulation method. We get that NSPK is insecure even with only one corrupted party while the fixed version is secure as long as there are two honest parties.
bisimulation observational equivalence security protocols authentication
Xiaojuan Cai Xiaohong Wu
BASICS Laboratory, Department of Computer Science Shanghai Jiao Tong University, Shanghai, China 200 Department of Computer Science and Technology, Huzhou Teachers College, Zhejiang, China, 313000
国际会议
Second International Symposium on Electronic Commerce and Security(第二届电子商务与安全国际研究大会)(ISECS 2009)
南昌
英文
1042-1046
2009-05-22(万方平台首次上网日期,不代表论文的发表时间)