收稿日期: 2003-05-16
修回日期: 2003-07-01
网络出版日期: 2004-05-10
基金资助
国家自然科学基金项目 (60102004;60273027;60025205)资助
Running-Mode Analysis of the Three-Party Cryptographic Protocol
Received date: 2003-05-16
Revised date: 2003-07-01
Online published: 2004-05-10
刘秀英 , 张玉清 , 杨波 , 邢戈 . 三方密码协议运行模式分析法[J]. 中国科学院大学学报, 2004 , 21(3) : 380 -385 . DOI: 10.7523/j.issn.2095-6134.2004.3.015
Based on the model checking theory, we derive the running mode analysis method of three party cryptographic protocols from the running mode analysis method of two party cryptographic protocols. To test this method, we use it to analyze the Davis Swick protocol and successfully prove the security of protocol. Therefore, we can draw a conclusion that running mode analysis of three party cryptographic protocol is available.
[1] Martin Abadi, Mark R Tuttle.A semantics for a logic of authentication (ExtendedAbstract).In:Proceedings of the 10th Annual ACM Symposium on Principles of Distributed Computing.1991.201-216
[2] L Paulson.The inductive approach to verifying cryptographic protocols.Journal of Computer Security, 1998, 6:85-128
[3] Gavin Lowe, A W Roscoe.Using CSP to detect errors in the TMN protocol.IEEE Transactions on Software Engineering, 1997, 23(10):659-669
[4] Catherine Meadows.The NRL protocol analyzer:An overview.Journal of Logic Programming, 1996, 26(2):113-131
[5] Z Dang, R A Kemmerer.Using the ASTRAL model checker for cryptographic protocol analysis.In:Proceedings of the DIMACS Workshop on Design andFormal Verification of Security Protocols.Available via URL, 1997;http://dimacs.rutgers.edu/Workshops/Security/program2/program.html
[6] J CMitchell, M Mitchell, U Stern.Automated analysis of cryptographic protocols using Murφ.In:Proceedingsof the IEEESymposium on Security and Privacy.IEEE Computer Society Press, 1997.141-151
[7] Yu-Qing ZHANG, Ji-Hong LI, Guo-Zhen XIAO.An approach to the formal verification of the two party cryptographic protocols.ACM Operating Systems Review, 1999, 33(4):48-51
[8] Will Marrero, Edmund Clarke, Somesh Jha.Model checking for security protocols.Technical Report CMU-SCS-97-139, Carnegie Mellon University, 1997
[9] Gavin Lowe.Towards a completeness result formodel checking of security protocols.Journal of Computer Security, 1999, 7(2-3):89-146
/
| 〈 |
|
〉 |
