Abstract
In experiments with a resolution-based verification method for cryptographic protocols, we could enforce its termination by tagging, a syntactic transformation of messages that leaves attack-free executions invariant. In this paper, we generalize the experimental evidence: we prove that the verification method always terminates for tagged protocols.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
M. Abadi and B. Blanchet. Analyzing Security Protocols with Secrecy Types and Logic Programs. In 29th ACM Symp. on Principles of Programming Languages (POPL’02), pages 33–44, Jan. 2002.
M. Abadi and R. Needham. Prudent engineering practice for cryptographic protocols. IEEE Transactions on Software Engineering, 22(1):6–15, Jan. 1996.
R. Amadio and W. Charatonik. On Name Generation and Set-Based Analysis in the Dolev-Yao Model. In CONCUR’02–Concurrency Theory, volume 2421 of LNCS, pages 499–514. Springer, Aug. 2002.
B. Blanchet. An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In 14th IEEE Computer Security Foundations Workshop (CSFW-14), pages 82–96, June 2001.
B. Blanchet. From Secrecy to Authenticity in Security Protocols. In 9th Internat. Static Analysis Symposium (SAS’02), volume 2477 of LNCS, pages 342–359. Springer, Sept. 2002.
P. Broadfoot, G. Lowe, and B. Roscoe. Automating Data Independence. In 6th European Symp. on Research in Computer Security (ESORICS’00), volume 1895 of LNCS, pages 175–190. Springer, Oct. 2000.
P. J. Broadfoot and A. W. Roscoe. Capturing Parallel Attacks within the Data Independence Framework. In 15th IEEE Computer Security Foundations Workshop (CSFW’02), pages 147–159, June 2002.
M. Burrows, M. Abadi, and R. Needham. A Logic of Authentication. Proceedings of the Royal Society of London A, 426:233–271, 1989.
E. Cohen. TAPS: A First-Order Verifier for Cryptographic Protocols. In 13th IEEE Computer Security Foundations Workshop (CSFW-13), pages 144–158, 2000.
H. Comon, V. Cortier, and J. Mitchell. Tree Automata with One Memory, Set Constraints, and Ping-Pong Protocols. In Automata, Languages and Programming, 28th Internat. Colloq., ICALP’01, volume 2076 of LNCS, pages 682–693. Springer, July 2001.
R. Corin and S. Etalle. An Improved Constraint-Based System for the verification of Security Protocols. In 9th Internat. Static Analysis Symposium (SAS’02), volume 2477 of LNCS, pages 326–341. Springer, Sept. 2002.
V. Cortier, J. Millen, and H. Rueß. Proving secrecy is easy enough. In 14th IEEE Computer Security Foundations Workshop (CSFW-14), pages 97–108, June 2001.
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), July 1999.
A. Gordon and A. Jeffrey. Authenticity by Typing for Security Protocols. In 14th IEEE Computer Security Foundations Workshop (CSFW-14), pages 145–159, June 2001.
J. Goubault-Larrecq. A Method for Automatic Cryptographic Protocol verification (Extended Abstract), invited paper. In 5th Internat. Workshop on Formal Methods for Parallel Programming: Theory and Applications (FMPPTA’00), volume 1800 of LNCS, pages 977–984. Springer, May 2000.
J. Heather, G. Lowe, and S. Schneider. How to Prevent Type Flaw Attacks on Security Protocols. In 13th IEEE Computer Security Foundations Workshop (CSFW-13), pages 255–268, July 2000.
J. Heather and S. Schneider. Towards automatic verification of authentication protocols on an unbounded network. In 13th IEEE Computer Security Foundations Workshop (CSFW-13), pages 132–143, July 2000.
G. Lowe. Breaking and Fixing the Needham-Schroeder Public-Key Protocol using FDR. In Tools and Algorithms for the Construction and Analysis of Systems, volume 1055 of LNCS, pages 147–166. Springer, 1996.
J. Millen and V. Shmatikov. Constraint Solving for Bounded-Process Cryptographic Protocol Analysis. In 8th ACM Conf. on Computer and Communications Security (CCS’01), pages 166–175, 2001.
F. Nielson, H. R. Nielson, and H. Seidl. Cryptographic Analysis in Cubic Time. In TOSCA 2001-Theory of Concurrency, Higher Order Languages and Types, volume 62 of ENTCS, Nov. 2001.
L. C. Paulson. The Inductive Approach to Verifying Cryptographic Protocols. J. Computer Security, 6(1–2):85–128, 1998.
A.W. Roscoe and P. J. Broadfoot. Proving Security Protocols with Model Checkers by Data Independence Techniques. J. Computer Security, 7(2, 3):147–190, 1999.
M. Rusinovitch and M. Turuani. Protocol Insecurity with Finite Number of Sessions is NP-complete. In 14th IEEE Computer Security Foundations Workshop (CSFW-14), pages 174–187, June 2001.
C. Weidenbach. Towards an Automatic Analysis of Security Protocols in First-Order Logic. In 16th Internat. Conf. on Automated Deduction (CADE-16), volume 1632 of LNAI, pages 314–328. Springer, July 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Blanchet, B., Podelski, A. (2003). Verification of Cryptographic Protocols: Tagging Enforces Termination. In: Gordon, A.D. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2003. Lecture Notes in Computer Science, vol 2620. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36576-1_9
Download citation
DOI: https://doi.org/10.1007/3-540-36576-1_9
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00897-2
Online ISBN: 978-3-540-36576-1
eBook Packages: Springer Book Archive