Skip to main content
SpringerLink
Log in

On the Decidability of Cryptographic Protocols with Open-Ended Data Structures

  • Conference paper
  • First Online:
CONCUR 2002 — Concurrency Theory (CONCUR 2002)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2421))

Included in the following conference series:

Abstract

Formal analysis of cryptographic protocols has mainly concentrated on protocols with closed-ended data structures, where closedended data structure means that the messages exchanged between principals have fixed and finite format. However, in many protocols the data structures used are open-ended, i.e., messages have an unbounded number of data fields. Formal analysis of protocols with open-ended data structures is one of the challenges pointed out by Meadows. This work studies decidability issues for such protocols. We propose a protocol model in which principals are described by transducers, i.e., finite automata with output, and show that in this model security is decidable and PSPACE-hard in presence of the standard Dolev-Yao intruder.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. M. Amadio and W. Charatonik. On name generation and set-based analysis in Dolev-Yao model. Technical Report RR-4379, INRIA, 2002.

    Google Scholar 

  2. R. M. Amadio, D. Lugiez, and V. Vanackère. On the symbolic reduction of processes with cryptographic functions. Technical Report RR-4147, INRIA, 2001.

    Google Scholar 

  3. G. Ateniese, M. Steiner, and G. Tsudik. Authenticated group key agreement and friends. In Proceedings of the 5th ACM Conference on Computer and Communication Secruity (CCS’98), pages 17–26, San Francisco, CA, 1998. ACM Press.

    Google Scholar 

  4. J. Bryans and S. A. Schneider. CSP, PVS, and a Recursive Authentication Protocol. In DIMACS Workshop on Formal Verification of Security Protocols, 1997.

    Google Scholar 

  5. J. A. Bull and D. J. Otway. The authentication protocol. Technical Report DRA/CIS3/PROJ/CORBA/SC/1/CSM/436-04/03, Defence Research Agency, Malvern, UK, 1997.

    Google Scholar 

  6. D. Dolev, S. Even, and R. M. Karp. On the Security of Ping-Pong Protocols. Information and Control, 55:57–68, 1982.

    Article  MATH  MathSciNet  Google Scholar 

  7. D. Dolev and A. C. Yao. On the Security of Public-Key Protocols. IEEE Transactions on Information Theory, 29(2):198–208, 1983.

    Article  MATH  MathSciNet  Google Scholar 

  8. N. A. Durgin, P. D. Lincoln, J. C. Mitchell, and A. Scedrov. Undecidability of bounded security protocols. In Workshop on Formal Methods and Security Protocols (FMSP’99), 1999.

    Google Scholar 

  9. S. Even and O. Goldreich. On the Security of Multi-Party Ping-Pong Protocols. In IEEE Symposium on Foundations of Computer Science (FOCS’83), pages 34–39, 1983.

    Google Scholar 

  10. N. Ferguson and B. Schneier. A Cryptographic Evaluation of IPsec. Technical report, 2000. Available from http://www.counterpane.com/ipsec.pdf.

  11. M. R. Garey and D. S. Johnson. Computers and Intractability: A Guide to the Theory of NP-Completeness. Freeman, San Francisco, 1979.

    MATH  Google Scholar 

  12. D. Harkins and D. Carrel. The Internet Key Exchange (IKE), November 1998. RFC 2409.

    Google Scholar 

  13. A. Huima. Efficient infinite-state analysis of security protocols. In Workshop on Formal Methods and Security Protocols (FMSP’99), 1999.

    Google Scholar 

  14. R. Küsters. On the Decidability of Cryptographic Protocols with Open-ended Data Structures. Technical Report IFI-0204, CAU Kiel, Germany, 2002. Available from http://www.informatik.uni-kiel.de/reports/2002/0204.html.

  15. C. Meadows. Extending formal cryptographic protocol analysis techniques for group protocols and low-level cryptographic primitives. In Proceedings of the First Workshop on Issues in the Theory of Security (WITS’00), pages 87–92, 2000.

    Google Scholar 

  16. C. Meadows. Open issues in formal methods for cryptographic protocol analysis. In Proc. of DISCEX 2000, pages 237–250. IEEE Computer Society Press, 2000.

    Google Scholar 

  17. J. Mitchell, M. Mitchell, and U. Stern. Automated Analysis of Cryptographic Protocols using Murphi. In Proceedings of the 1997 IEEE Symposium on Security and Privacy, pages 141–151. IEEE Computer Society Press, 1997.

    Google Scholar 

  18. L. C. Pauslon. Mechanized proofs for a recursive authetication protocol. In 10th IEEE Computer Security Foundations Workshop (CSFW-10), pages 84–95, 1997.

    Google Scholar 

  19. O. Pereira and J.-J. Quisquater. A Security Analysis of the Cliques Protocols Suites. In Proceedings of the 14th IEEE Computer Security Foundations Workshop (CSFW-14), pages 73–81, 2001.

    Google Scholar 

  20. M. Rusinowitch and M. Turuani. Protocol Insecurity with Finite Number of Sessions is NP-complete. In 14th IEEE Computer Security Foundations Workshop (CSFW-14), pages 174–190, 2001.

    Google Scholar 

  21. M. Steiner, G. Tsudik, and M. Waidner. CLIQUES: A new approach to key agreement. In IEEE International Conference on Distributed Computing Systems. IEEE Computer Society Press, pages 380–387, 1998.

    Google Scholar 

  22. J. Zhou. Fixing a security flaw in IKE protocols. Electronic Letter, 35(13):1072–1073, 1999.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel, Germany

    Ralf Küsters

Authors
  1. Ralf Küsters
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Faculty of Informatics, Masaryk University Brno, Botanicka 68a, 60200, Brno, Czech Republic

    Luboš Brim , Mojmír Křetínský  & Antonín Kučera ,  & 

  2. Faculty of Electrical Engineering and Informatics, Department of Computer Science, Technical University of Ostrava (VSB), 17. listopadu 15, 70833, Ostrava-Poruba, Czech Republic

    Petr Jančar

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Küsters, R. (2002). On the Decidability of Cryptographic Protocols with Open-Ended Data Structures. In: Brim, L., Křetínský, M., Kučera, A., Jančar, P. (eds) CONCUR 2002 — Concurrency Theory. CONCUR 2002. Lecture Notes in Computer Science, vol 2421. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45694-5_34

Download citation

  • DOI: https://doi.org/10.1007/3-540-45694-5_34

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-44043-7

  • Online ISBN: 978-3-540-45694-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation