Local abstract verification and refinement of security protocols

ABSTRACT

The verification problem for security protocols is undecidable, but it is feasible to verify protocols by abstract interpretation. This paper presents a method based on local abstraction and refinement for verifying security protocols terminably. Local abstraction produces a safe approximation of the security protocol, modeled as a set of Horn logic rules. Refinement removes false attacks introduced by local abstraction. In contrast with methods based on global abstraction, our method abstracts only certain rules that can lead to non-termination when computing fixpoints, that is, it does not abstract all rules. We implement this method in a verification tool SPVT and are able to verify well-known protocols. Moreover, our experiments indicate that local abstraction is less costly than global abstraction.

REFERENCES

• 1: Michael Backes , Agostino Cortesi , Matteo Maffei, Causality-based Abstraction of Multiplicity in Security Protocols, Proceedings of the 20th IEEE Computer Security Foundations Symposium, p.355-369, July 06-08, 2007 [doi>10.1109/CSF.2007.11]
• 2: B. Blanchet. ProVerif Automatic Cryptographic Protocol Verifier User Manual. CNRS, Département d'Informatique École Normale Supérieure, Paris.
• 3: Bruno Blanchet, An Efficient Cryptographic Protocol Verifier Based on Prolog Rules, Proceedings of the 14th IEEE workshop on Computer Security Foundations, p.82, June 11-13, 2001
• 4: Bruno Blanchet, From Secrecy to Authenticity in Security Protocols, Proceedings of the 9th International Symposium on Static Analysis, p.342-359, September 17-20, 2002
• 5: Bruno Blanchet , Andreas Podelski, Verification of cryptographic protocols: tagging enforces termination, Theoretical Computer Science, v.333 n.1-2, p.67-90, 1 March 2005 [doi>10.1016/j.tcs.2004.10.018]
• 6: L. Bozga, Y. Lakhnech, and M. Périn. HERMES: An automatic tool for verification of secrecy in security protocols. In CAV, pages 219--222, 2003.
• 7: L. Bozga , Y. Lakhnech , M. Périn, Pattern-based abstraction for verifying secrecy in protocols, International Journal on Software Tools for Technology Transfer (STTT), v.8 n.1, p.57-76, February 2006 [doi>10.1007/s10009-005-0189-6]
• 8: J. A. Clark and J. L. Jacob. A survey of authentication protocol literature. Technical Report 1.0, 1997.
• 9: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 10: N. Durgin, P. Lincoln, J. Mitchell, and A. Scedrov. Undecidability of bounded security protocols. In N. Heintze and E. Clarke, editors, Proceedings of the Workshop on Formal Methods and Security Protocols -- FMSP, Trento, Italy, July 1999.
• 11: M. Li, Z. Li, H. Chen, and T. Zhou. A novel derivation framework for definite logic program. In P. Panangaden, Y. Chen, and G. Zhang, editors, FICS 2008, volume 212, pages 71--85, Amsterdam, The Netherlands, The Netherlands, June 2008. Elsevier Science Publishers B. V.
• 12: M. Li, T. Zhou, Z. Li, and H. Chen. An abstraction and refinement framework for verifying security protocols based on logic programming. In I. Cervesato, editor, ASIAN 2007, volume 4846 of Lecture Notes in Computer Science, pages 166--180, Berlin Heidelberg, 12 2007. Springer-Verlag.
• 13: 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
• 14: F. Oehl, G. Cece, O. Kouchnarenko, and D. Sinclair. Automatic approximation for the verification of cryptographic protocols, 2003.

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS
      C.2.0 General
          Subjects: Security and protection (e.g., firewalls)

Additional Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS
      C.2.2 Network Protocols
          Subjects: Protocol verification

  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification

General Terms:
Languages, Security, Theory, Verification

Keywords:
abstraction, refinement, security protocols, verification