An approach to the formal verification of the three-principal cryptographic protocols

ABSTRACT

Based on the model checking theory, we derive the Running-Mode Analysis of three-principal cryptographic protocols from the Running-Mode Analysis of two-principal cryptographic protocols. To test this method, we analyze the Davis Swick protocol and successfully prove the security this protocol. Therefore, we can draw a conclusion that Running-Mode Analysis of three-principal cryptographic protocol is available.

REFERENCES

• 1: Michael Burrows , Martin Abadi , Roger Needham, A logic of authentication, ACM Transactions on Computer Systems (TOCS), v.8 n.1, p.18-36, Feb. 1990 [doi>10.1145/77648.77649]
• 2: Z. Dang and R. A. Kemmerer. Using the ASTRAL Model Checker for Cryptographic Protocol Analysis. In Proceedings of the DIMACS Workshop on Design and Formal Verification of Security Protocols, 1997. Available via URL: http://dimacs.rutgers.edu/Workshops/Security/program2/program.html
• 3: Gavin Lowe, Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR, Proceedings of the Second International Workshop on Tools and Algorithms for Construction and Analysis of Systems, p.147-166, March 27-29, 1996
• 4: Gavin Lowe, Towards a completeness result for model checking of security protocols, Journal of Computer Security, v.7 n.2-3, p.89-146, Jan. 1999
• 5: Gavin Lowe , Bill Roscoe, Using CSP to Detect Errors in the TMN Protocol, IEEE Transactions on Software Engineering, v.23 n.10, p.659-669, October 1997 [doi>10.1109/32.637148]
• 6: Catherine Meadows. The NRL Protocol Analyzer: An Overview. Journal of Logic Programming, 1996, 26(2): 113--131.
• 7: J. C. Mitchell , M. Mitchell , U. Stern, Automated analysis of cryptographic protocols using Mur/spl phi/, Proceedings of the 1997 IEEE Symposium on Security and Privacy, p.141, May 04-07, 1997
• 8: Will Marrero, Edmund Clarke, Somesh Jha. Model Checking for Security Protocols. Technical Report CMU-SCS-97-139, Carnegie Mellon University, May 1997.
• 9: Lawrence C. Paulson, The inductive approach to verifying cryptographic protocols, Journal of Computer Security, v.6 n.1-2, p.85-128, Sept. 1998
• 10: Yuqing Zhang , Jihong Li , Guozhen Xiao, An approach to the formal verification of the two-party cryptographic protocols, ACM SIGOPS Operating Systems Review, v.33 n.4, p.48-51, Oct. 1999 [doi>10.1145/334598.334607]