Journal of University of Chinese Academy of Sciences >
Running-Mode Analysis of the Three-Party Cryptographic Protocol
Received date: 2003-05-16
Revised date: 2003-07-01
Online published: 2004-05-10
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.
LIU XiuYing , ZHANG YuQing , YANG Bo , XING Ge . Running-Mode Analysis of the Three-Party Cryptographic Protocol[J]. Journal of University of Chinese Academy of Sciences, 2004 , 21(3) : 380 -385 . DOI: 10.7523/j.issn.2095-6134.2004.3.015
[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
/
| 〈 |
|
〉 |