skip to main content
10.1145/1456396.1456399acmconferencesArticle/Chapter ViewAbstractPublication PagesccsConference Proceedingsconference-collections
research-article

Local abstract verification and refinement of security protocols

Authors Info & Claims
Published:27 October 2008Publication History

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. M. Backes, A. Cortesi, and M. Maffei. Causality-based abstraction of multiplicity in security protocols. In Proceedings of 20th IEEE Computer Security Foundation Symposium (CSF), June 2007. Google ScholarGoogle ScholarDigital LibraryDigital Library
  2. B. Blanchet. ProVerif Automatic Cryptographic Protocol Verifier User Manual. CNRS, Département d'Informatique École Normale Supérieure, Paris.Google ScholarGoogle Scholar
  3. B. Blanchet. An efficient cryptographic protocol verifier based on prolog rules. In 14th IEEE Computer Security Foundations Workshop (CSFW-14), pages 82--96, 2001. Google ScholarGoogle ScholarDigital LibraryDigital Library
  4. B. Blanchet. From secrecy to authenticity in security protocols. In M. Hermenegildo and G. Puebla, editors, 9th International Static Analysis Symposium (SAS'02), volume 2477 of Lecture Notes in Computer Science, pages 342--359, Madrid, Spain, September 2002. Springer Verlag. Google ScholarGoogle ScholarDigital LibraryDigital Library
  5. B. Blanchet and A. Podelski. Verification of cryptographic protocols: tagging enforces termination. Theoretical Computer Science, 333(1--2):67--90, March 2005. Google ScholarGoogle ScholarDigital LibraryDigital Library
  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.Google ScholarGoogle Scholar
  7. L. Bozga, Y. Lakhnech, and M. Périn. Pattern-based abstraction for verifying secrecy in protocols. Int. J. Softw. Tools Technol. Transf., 8(1):57--76, 2006. Google ScholarGoogle ScholarDigital LibraryDigital Library
  8. J. A. Clark and J. L. Jacob. A survey of authentication protocol literature. Technical Report 1.0, 1997.Google ScholarGoogle Scholar
  9. P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 238--252, Los Angeles, California, 1977. ACM Press, New York, NY. Google ScholarGoogle ScholarDigital LibraryDigital Library
  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.Google ScholarGoogle Scholar
  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.Google ScholarGoogle Scholar
  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. Google ScholarGoogle ScholarDigital LibraryDigital Library
  13. G. Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In T. Margaria and B. Steffen, editors, TACAS, volume 1055 of Lecture Notes in Computer Science, pages 147--166. Springer, 1996. Google ScholarGoogle ScholarDigital LibraryDigital Library
  14. F. Oehl, G. Cece, O. Kouchnarenko, and D. Sinclair. Automatic approximation for the verification of cryptographic protocols, 2003.Google ScholarGoogle Scholar

Index Terms

  1. Local abstract verification and refinement of security protocols

          Recommendations

          Comments

          Login options

          Check if you have access through your login credentials or your institution to get full access on this article.

          Sign in
          • Published in

            cover image ACM Conferences
            FMSE '08: Proceedings of the 6th ACM workshop on Formal methods in security engineering
            October 2008
            70 pages
            ISBN:9781605582887
            DOI:10.1145/1456396

            Copyright © 2008 ACM

            Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

            Publisher

            Association for Computing Machinery

            New York, NY, United States

            Publication History

            • Published: 27 October 2008

            Permissions

            Request permissions about this article.

            Request Permissions

            Check for updates

            Qualifiers

            • research-article

            Upcoming Conference

            CCS '24
            ACM SIGSAC Conference on Computer and Communications Security
            October 14 - 18, 2024
            Salt Lake City , UT , USA
          • Article Metrics

            • Downloads (Last 12 months)1
            • Downloads (Last 6 weeks)0

            Other Metrics

          PDF Format

          View or Download as a PDF file.

          PDF

          eReader

          View online with eReader.

          eReader