Abstract
The rationale of authentication has been a topic of study for about a decade and a half. First attempts at formal analysis of authentication protocols were not using logics per se, but were certainly logical. Millen’s Interrogator [Mil84, MCF87] was a Prolog based tool specifically designed for authentication protocol analysis that functioned essentially as a special purpose model checker. Kemmerer used the general purpose formal specification language Ina Jo and an accompanying symbolic execution tool Inatest to specify and analyze protocols [Kem87].
This paper is based on a course Syverson taught at the 1st International School on Foundations of Security Analysis and Design (FOSAD’00) in Bertinoro, Italy in September 2000. Cervesato was a student there. The work of the first author was supported by ONR. The work of the second author was supported by NSF grant INT98-15731 “Logical Methods for Formal Verification of Software” and by NRL under contract N00173-00-C-2086.
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, M. Burrows, C. Kaufman, and B. Lampson. Authentication and delegation with smart-cards. Research Report 67, Digital Systems Research Center, October 1990. Revised July, 1992. 69
MartĂn Abadi and Andrew D. Gordon. A calculus for cryptographic protocols: the spi calculus. In Proceedings of the Fourth ACM Conference on Computer and Communications Security, pages 36–47. ACM Press, April 1997. 130
MartĂn Abadi and Andrew D. Gordon. A calculus for cryptographic protocols: the spi calculus. Information and Computation, 143:1–70, 1999. An extended version of this paper appears as Research Report 149, Digital Equipment Corporation Systems Research Center, January 1998. An early presentation appears in [AG97]. 113
MartĂn Abadi and Roger Needham. Prudent engineering practices for cryptographic protocols. In Proceedings of the IEEE Computer Society Symposium on Research in Security and Privacy, pages 122–136. IEEE CS Press, May 1994. 106, 130
Ross Anderson and Roger Needham. Robustness principles for public key protocols. In D. Coppersmith, editor, Advances in Cryptology — CRYPTO’ 95, pages 236–247. Springer-Verlag, LNCS 963, August 1995. 107, 109
MartĂn Abadi and Roger Needham. Prudent engineering practices for cryptographic protocols. IEEE Transactions on Software Engineering, 22(1):6–15, January 1996. A preliminary version appeared as [AN94]. 106
The anonymizer. http://www.anonymizer.com. 128
MartĂn Abadi and Phillip Rogaway. Reconciling two views of cryptographic protocols (the compuational soundness of formal encryption. In IFIP International Conference on Theoretical Computer Science (IFIP TCS2000). Springer-Verlag, LNCS, 2000. 128
Giuseppe Ateniese, Michael Steiner, and Gene Tsudik. Authenticated group key agreement and friends. In 5th ACM Conference on Computer and Communications Security (CCS’98), pages 17–26. ACM Press, November 1998.126
MartĂn Abadi and Mark R. Tuttle. A semantics for a logic of authentication. In Proceedings of the Tenth Annual ACM Symposium on Principles of Distributed Computing, pages 201–216. ACM Press, August 1991. 67, 76, 79,88, 95, 120, 124, 125
Michael Burrows, MartĂn Abadi, and Roger Needham. Authentication: A practical study of belief in action. In M. Vardi, editor, Proceedings of the Second Conference on Theoretical Aspects of Reasoning About Knowledge (Tark), pages 325–342. Morgan Kaufmann, March 1988. Also presented at The Computer Security Foundations Workshop, Franconia, NH, June 1988.66
Michael Burrows, MartĂn Abadi, and Roger Needham. A logic of authentication. Research Report 39, Digital Systems Research Center, February 1989. Revised Feb. 22, 1990. 63, 66, 67, 68, 69, 70, 85, 87, 93, 95, 98, 101, 102
Michael Burrows, MartĂn Abadi, and Roger Needham. A logic of authentication. Operating Systems Review, 23(5):1–13, December 1989. This issue of OSR: Proceedings of the Twelfth ACM Symposium on Operating Systems Principles (SOSP), Litchfield Park, Arizona, December 1989. 66
Michael Burrows, MartĂn Abadi, and Roger Needham. A logic of authentication. Proceedings of the Royal Society of London. Series A, Mathematical and Physical Sciences, 426(1871):233–271, December 1989. 66
Michael Burrows, MartĂn Abadi, and Roger Needham. A logic of authentication. ACM Transactions on Computer Systems, 8(1):18–36, Feb 1990.66
Michael Burrows, MartĂn Abadi, and Roger Needham. Rejoinder to nessett. Operating Systems Review, 24(2):39–40, April 1990. 75
Michael Burrows, MartĂn Abadi, and Roger Needham. The scope of a logic of authentication. In J. Feigenbaum and M. Merritt, editors, Distributed Computing and Cryptography, volume 2 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 119–126. AMS and ACM, 1990. Proceedings of a DIMACS workshop, October 1989. 66
Pierre Bieber. A logic of communication in hostile environment. In Proceedings of the Computer Security Foundations Workshop III, pages 14–22. IEEE CS Press, June 1990. 97, 98
Steven M. Bellovin and Michael Merritt. Encrypted key exchange: Passwordbased protocols secure against dictionary attacks. In Proceedings of the IEEE Computer Society Symposium on Research in Security and Privacy, pages 72–84IEEE CS Press, May 1992. 108
Steve Bellovin and Michael Merritt. Augmented encrypted key exchange: a password-based protocol secure against dictionary attacks and password file compromise. In Proceedings of the 1st ACM Conference on Computer and Communications Security, pages 244–250. ACM Press, November 1993. 108
Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson, and Piero Tramontano. Formal verification of cardholder registration in SET. In F. Cuppens, Y. Deswarte, D. Gollmann, and M. Waidner, editors, Computer Security-ESORICS 2000, pages 159–174. Springer-Verlag, LNCS 1895, October 2000. 127
Stephen H. Brackin. A HOL extension of GNY for automatically analyzing cryptographic protocols. In 9th IEEE Computer Security Foundations Workshop, pages 62–76. IEEE CS Press, June 1996. 112
Stephen H. Brackin. Automatic formal analyses of two large commercial protocols. In DIMACS Workshop on Design and Formal Verification of Security Protocols, September 1997. Available at http://dimacs.rutgers.edu/Workshops/Security/program2/brackin.html. 112, 127
Stephen H. Brackin. Evaluating and improving protocol analysis by automatic proof. In 1.Mathematical Models of Computer Security 11th IEEE Computer Security Foundations Workshop, pages 138–152. IEEE CS Press, 1998. 112
Stephen H. Brackin. Automatically detecting most vulnerabilities in cryptographic protocols. In DISCEX 2000: Proceedings of the DARPA Information Survivability Conference and Exposition, volume I, pages 222–236. IEEE CS Press, January 2000. 112
Jeremy Bryans and Steve Schneider. CSP, PVS and a recursive authentication protocol. In DIMACS Workshop on Design and Formal Verification of Security Protocols, September 1997. Available at http://dimacs.rutgers.edu/Workshops/Security/program2/program.html. 126
Levente Buttyán, Sebastian Staamann, and Uwe Wilhelm. A simple logic for authentication protocol design. In 11th IEEE Computer Security Foundations Workshop, pages 153–162. IEEE CS Press, June 1998. 113
Ran Canetti. A unified framework for analyzing security of protocols. Cryptology ePrint Archive, Report 2000/067, 2000. http://eprint.iacr.org.128
Ulf Carlsen. Using Logics to Detect Implementation-Dependent Flaws. In Proceedings of the Ninth Annual Computer Security Applications Conference, pages 64–73. IEEE Computer Society Press, December 1993. 93
Ulf Carlsen. Generating formal cryptographic protocol specifications. In Proceedings of the IEEE Computer Society Symposium on Research in Security and Privacy, pages 137–146. IEEE CS Press, May 1994. 98
Iliano Cervesato, Nancy Durgin, Patrick Lincoln, John Mitchell, and Andre Scedrov. A comparison between strand spaces and transition systems for the specification of security protocols. To appear as a technical report, Department of Computer Science, Stanford University. 118
David Chaum. Blind signatures for untraceable payments. In D. Chaum, R. L. Rivest, and A. T. Sherman, editors, Advances in Cryptology-Proceedings of Crypto 82, pages 199–203, 1983. 107
David Chaum. The dining cryptographers problem: Unconditional sender and receiver untraceability. Journal of Cryptology, 1(1):65–75, 1988. 128
Brian F. Chellas. Modal Logic: An Introduction. Cambridge University Press, 1980. 78, 79
John Clark and Jeremy Jacob. A survey of authentication protocol literature: Version 1.0, nov 1997. Available at http://www-users.cs.york.ac.uk/~jac/ under the link “Security Protocols Review”. 87, 93, 102, 103, 112
John Clark and Jeremy Jacob. Searching for a solution: Engineering tradeoffs and the evolution of provably secure protocols. In Proceedings of the IEEE Symposium on Security and Privacy, pages 82–95. IEEE CS Press, May 2000. 113
Ran Canetti, Catherine Meadows, and Paul Syverson. Environmental requirements and authentication protocols. In Proceedings of the Symposium on Requirements Engineering for Information Security (SREIS), March 2001. A version of this paper has been invited for a special issue of Requirements Engineering. 128
Crowds. http://www.research.att.com/projects/crowds/. 128
Jan L. Camenisch and Markus A. Stadler. Efficient group signature schemes for large groups. In B. Kaliski, editor, Advances in Cryptology-CRYPTO’ 97, pages 410–424. Springer-Verlag, LNCS 1294, 1997. 126
David Chaum and Eugène van Heyst. Group signature. In D. W. Davies, editor, Advances in Cryptology-EUROCRYPT’ 91, pages 257-265. Springer-Verlag, LNCS 547, 1991. 126
Anthony H. Dekker. C3po: a tool for automatic sound cryptographic protocol analysis. In 13th IEEE Computer Security Foundations Workshop, pages 77–87IEEE CS Press, June 2000. 83, 113
Naganand Doraswamy and Dan Harkins. IPSEC: The New Security Standard for the Internet, Intranets, and Virtual Private Networks. Prentice Hall, 1999.76, 125
G. Denker and J. Millen. Capsl integrated protocol environment. In DISCEX 2000: Proceedings of the DARPA Information Survivability Conference and Exposition, volume I, pages 207–221. IEEE CS Press, January 2000. 112
Dorothy E. Denning and Giovanni Maria Sacco. Timestamps in key distribution protocols. Communications of the ACM, 24(8):533–536, August 1981. 73, 92
Whitfield Diffie, Paul C. van Oorschot, and Michael J. Wiener. Authentication and authenticated key exchanges. Designs, Codes, and Cryptography, 2:107–125, 1992. 104
Danny Dolev and Andrew C. Yao. On the security of public-key protocols. IEEE Transactions on Information Theory, 2(29):198–208, March 1983. 64,123
Neil Evans and Steve Schneider. Analysing time dependent security properties in CSP using PVS. In F. Cuppens, Y. Deswarte, D. Gollmann, and The Logic of Authentication Protocols 133 M. Waidner, editors, Computer Security-ESORICS 2000, pages 222–237. Springer-Verlag, LNCS 1895, October 2000. 103
Ronald Fagin, Joseph Y. Halpern, Yoram Moses, and Moshe Y. Vardi. Reasoning About Knowledge. MIT Press, 1995. 120, 121, 128
Freedom. http://www.freedom.net/. 128
Li Gong, Roger Needham, and Raphael Yahalom. Reasoning about Belief in Cryptographic Protocols. In Proceedings of the IEEE Computer Society Symposium on Research in Security and Privacy, pages 234–248. IEEE Computer Society Press, 1990. 76, 88, 89, 95
Robert Goldblatt. Logics of Time and Computation, 2nd edition, volume 7 of CSLI Lecture Notes. CSLI Publications, 1992. 79
Dieter Gollmann. What do we mean by entity authentication?In Proceedings of the IEEE Symposium on Security and Privacy, pages 46–54. IEEE CS Press, May 1996. 99
Dieter Gollmann. On the verification of cryptographic protocols-a tale of two committees. In Steve Schneider and Peter Ryan, editors, Electronic Notes in Theoretical Computer Science, volume 32. Elsevier Science Publishers, 2000.102, 105
Li Gong and Paul Syverson. Fail-stop protocols: An approach to designing secure protocols. In R. K. Iyer, M. Morganti, W. K. Fuchs, and V. Gligor, editors, Dependable Computing for Critical Applications 5, pages 79–100. IEEE Computer Society Press, 1998. 109
Joshua D. Guttman. Security goals: Packet trajectories and strand spaces. This volume. 113, 118
N. Heintze and J. D. Tygar. A model for secure protocols and their composition. IEEE Transactions on Software Engineering, 22(1):16–30, January 1996. 127
Jan JĂĽrjens. Bridging the gap: Formal vs. complexity-theoretical reasoning about cryptography, December 2000. Presentation at the Schloss Dagstuhl Seminar on Security through Analysis and Verification. 128
Rajashekar Kailar. Reasoning about accountability in protocols for electronic commerce. In Proceedings of the IEEE Symposium on Security and Privacy, pages 236–250. IEEE CS Press, May 1995. 127
Rajashekar Kailar. Accountability in electronic commerce protocols. IEEE Transactions on Software Engineering, 5(22), May 1996. 127
Richard A. Kemmerer. Using formal verification techniques to analyze cryptographic protocols. In Proceedings of the 1987 IEEE Symposium on Security and Privacy, pages 134–139. IEEE CS Press, May 1987. 63
Volker Kessler and Heike Neumann. A sound logic for analysing electronic commerce protocols. In J.-J. Quisquater, Y. Deswarte, C. Meadows, and D. Gollmann, editors, Computer Security-ESORICS 98, pages 345–360. Springer-Verlag, LNCS 1485, September 1998. 127
Steve Kremer and Jean-François Raskin. A game approach to the verification of exchange protocols: Application to non-repudiation protocols. In P. Degano, editor, First Workshop on Issues in the Theory of Security-WITS’00, pages 93–98, July 2000. 127
Leslie Lamport. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 21(7):558–565, July 1978. 109
G. Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. Software-Concepts and Tools, 17:93–102, 1996. 92, 101
Gavin Lowe. A herarchy of authentication specifications. In Proceedings of the 10th IEEE Computer Security Foundations Workshop (CSFW9), pages 31–43. IEEE Computer Society Press, June 1997. 100, 101, 102, 103
Jonathan K. Millen, Sidney C. Clark, and Sheryl B. Freedman. The Interrogator: Protocol security analysis. IEEE Transactions on Software Engineering, 13(2):274–288, 1987. 63
Catherine Meadows. A model of computation for the NRL Protocol Analyzer. In Proceedings of the 7th Computer Security Foundations Workshop, pages 84–89. IEEE CS Press, June 1994. 114, 116, 118
Catherine Meadows. The NRL Protocol Analyzer: An overview. Journal of Logic Programming, 26(2):113–131, February 1996. 114, 116
C. Meadows. Analysis of the Internet Key Exchange protocol using the NRL Protocol Analyzer. In Proceedings of the IEEE Symposium on Security and Privacy. IEEE Computer Society Press, May 1999. 128
Catherine Meadows. A formal framework and evaluation method for network denial of service. In Proceedings of the 12th IEEE Computer Security Foundations Workshop (CSFW12), pages 4–13. IEEE CS Press, June 1999.134
Catherine Meadows. Extending formal cryptographic protocol analysis techniques for group protocols and low-level cryptographic primitives. In P. Degano, editor, First Workshop on Issues in the Theory of Security-WITS’00, pages 87–92, July 2000. 126
Catherine Meadows. Open issues in formal methods for cryptographic protocol analysis. In DISCEX 2000: Proceedings of the DARPA Information Survivability Conference and Exposition, volume I, pages 237–250. IEEE Computer Society Press, January 2000. 125
Catherine Meadows. A cost-based framework for analysis of denial of service in networks. Journal of Computer Security, 2001. Forthcoming. A preliminary version of portions of this work appeared in [Mea99b]. 126
Elliott Mendelson. Introduction to Mathematical Logic. Wadsworth Publishing Co., 1987. 78
J. Millen. Capsl Web site. http://www.csl.sri.com/~millen/capsl. 112
Jonathan K. Millen. The Interrogator: A tool for cryptographic protocol security. In Proceedings of the 1984 IEEE Symposium on Security and Privacy, pages 134–141, Oakland, CA, April 1984. IEEE Computer Society Press. 63
Paul K. Moser, editor. Empirical Knowledge: Readings in Contemporary Epistemology. Rowman & Littlefield, 1986. 79
Jon Millen and Harald Rueff. Protocol-independent secrecy. In Proceedings of the IEEE Symposium on Security and Privacy, pages 110–119, May 2000. 123
C. Meadows and P. Syverson. A formal specification of requirements for payment trnasactions in the SET protocol. In R. Hirschfeld, editor, Financial Cryptography, FC’98, pages 122–140. Springer-Verlag, LNCS 1465, 1998. 117,127
Alfred J. Menezes, Paul C. van Oorschot, and Scott A. Vanstone. Handbook of Applied Cryptography. CRC Press, 1997. 64, 80, 89
D. M. Nessett. A critique of the burrows, abadi, and needham logic. Operating Systems Review, 24(2):35–38, April 1990. 73, 74
R. M. Needham and M. D. Schroeder. Using encryption for authentication in large networks of computers. Communications of the ACM, 21(12):993–999, 1978. 65, 101, 102
B. Clifford Neuman and Stuart G. Stubblebine. A Note on the Use of Timestamps as Nonces. Operating Systems Review, 27(2):10–14, April 1993. 93
Onion routing. http://www.onion-router.net/. 128
Lawrence C. Paulson. Mechanized proofs for a recursive authentication protocol. In Proceedings of the 10th IEEE Computer Security Foundations Workshop (CSFW10), pages 84–94. IEEE CS Press, June 1997. 126
Adrian Perrig and Dawn Song. Looking for diamonds in the desert — extending automatic protocol generation to three-party authentication and key agreement. In 13th IEEE Computer Security Foundations Workshop, pages 64–76. IEEE CS Press, June 2000. 113
A. W. Roscoe. Intensional specification of security protocols. In Proceedings of the 9th IEEE Computer Security Foundations Workshop (CSFW9), pages 28–36. IEEE CS Press, June 1996. 103
M. Satyanarayanan. Integrating security in a large distributed system. ACM Transactions on Computer Systems, 15(3):247–280, August 1989. 102
Bruce Schneier. Applied Cryptography, Second Edition: Protocols, Algorithms, and Source Code in C. John Wiley & Sons, 1996. 64, 80, 107
Secure Electronic Transaction Specification, Version 1.0, May 1997. http://www.visa.com/set/. 117
P. Syverson and C. Meadows. A logical language for specifying cryptographic protocol requirements. In Proceedings of the IEEE Computer Society Symposium on Research in Security and Privacy, pages 165–177. IEEE CS Press, May 1993. 117
P. Syverson and C. Meadows. Formal requirements for key distribution protocols. In A. De Santis, editor, Advances in Cryptology — EUROCRYPT’ 94, pages 32–331. Springer-Verlag, LNCS 950, 1994. 117
P. Syverson and C. Meadows. A formal language for cryptographic protocol requirements. Designs, Codes, and Cryptography, 7(1 and 2):27–59, January 1996. 114, 116, 117
Einar Snekkenes. Exploring the BAN approach to protocol analysis. In Proceedings of the IEEE Computer Society Symposium on Research in Security and Privacy, pages 171–181. IEEE CS Press, May 1991. 96, 97
Einar Snekkenes. Roles in cryptographic protocols. In Proceedings of the IEEE Computer Society Symposium on Research in Security and Privacy, pages 105–119. IEEE CS Press, May 1992. 98
Dawn Song. Athena: a new efficient automatic checker for security protocol analysis. In Proceedings of the Twelth IEEE Computer Security Foundations Workshop, pages 192–202, Mordano, Italy, June 1999. IEEE Computer Society Press. 118
Steve Schneider and Abraham Sidiropoulos. CSP and anonymity. In E. Bertino, H. Kurth, G. Martella, and E. Montolivio, editors, Computer Security-ESORICS 96, pages 198–218. Springer Verlag, LNCS 1146, 1996.129
Paul Syverson and Stuart Stubblebine. Group principals and the formalization of anonymity. In J. M. Wing, J. Woodcock, and J. Davies, editors, FM’99-Formal Methods, Vol. I, pages 814–833. Springer-Verlag, LNCS 1708, 1999.128, 129
Douglas R. Stinson. Cryptography: Theory and Practice. CRC Press, 1995.64
Paul F. Syverson and Paul C. van Oorschot. On unifying some cryptographic protocols. In Proceedings of the IEEE Computer Society Symposium on Research in Security and Privacy, pages 14–28. IEEE CS Press, May 1994. 77,78, 120, 125
Paul F. Syverson and Paul C. van Oorschot. A unified cryptographic protocol logic. NRL Publication 5540–227, Naval Research Lab, 1996. 77, 78, 79, 84,85, 88, 95, 98, 120, 124, 125, 126
Stuart Stubblebine and Rebecca Wright. An authentication logic supporting synchronization, revocation, and recency. In 3rd ACM Conference on Computer and Communications Security (CCS’96), pages 95–105. ACM Press, March 1996. 127
Paul F. Syverson. The use of logic in the analysis of cryptographic protocols. In Proceedings of the IEEE Computer Society Symposium on Research in Security and Privacy, pages 156–170. IEEE CS Press, May 1991. 75, 76
Paul F. Syverson. Knowledge, belief, and semantics in the analysis of cryptographic protocols. Journal of Computer Security, 1(3,4):317–334, 1992. 76,79
Paul F. Syverson. Adding time to a logic of authentication. In Proceedings of the First ACM Conference on Computer and Communications Security, pages 97–101, November, 1993. ACM Press. 96, 98, 121
Paul F. Syverson. On Key Distribution Protocols for Repeated Authentication. Operating Systems Review, 27(4):24–30, October 1993. 93
Paul Syverson. A taxonomy of replay attacks. In Proceedings of the Computer Security Foundations Workshop (CSFW7), pages 187–191. IEEE CS Press, June 1994. 91, 92, 93, 95, 98
Paul Syverson. Limitations on design principles for public key protocols. In Proceedings of the IEEE Symposium on Security and Privacy, pages 62–72. IEEE Computer Society Press, May 1996. 107, 108
Paul F. Syverson. Relating two models of computation for security protocols. In Workshop on Formal Methods and Security Protocols, Indianapolis, Indiana, June 1998. Available at http://www.cs.bell-labs.com/who/nch/fmsp/program.html. 118
Paul F. Syverson. Towards a strand semantics for authentication logic. Electronic Notes in Theoretical Computer Science, 20, 2000. Proceedings of MFPS XV (S. Brookes, A. Jung, M. Mislove and A. Scedrov, eds.), New Orleans, LA, April 1999. 114, 118
F. Javier Thayer Fábrega, Jonathan C. Herzog, and Joshua D. Guttman. Strand spaces. Technical report, The MITRE Corporation, November 1997. 66, 114, 118, 121
F. Javier Thayer Fábrega, Jonathan C. Herzog, and Joshua D. Guttman. Honest ideals on strand spaces. In Proceedings of the 1998 IEEE Computer Security Foundations Workshop — CSFW’11, pages 66–77. IEEE Computer Society Press, 1998. 123
F. Javier Thayer Fábrega, Jonathan C. Herzog, and Joshua D. Guttman. Strand spaces: Why is a security protocol correct? In Proceedings of the 1998 IEEE Symposium on Security and Privacy, pages 160–171, Oakland, CA, May 1998. IEEE Computer Society Press. 66, 114, 118
F. Javier Thayer Fábrega, Jonathan C. Herzog, and Joshua D. Guttman. Mixed strand spaces. In P. Syverson, editor, Proceedings of the 12th IEEE Computer Security Foundations Workshop — CSFW’99, pages 72–82, Mordano, Italy, June 1999. IEEE Computer Society Press. 128
F. Javier Thayer Fábrega, Jonathan C. Herzog, and Joshua D. Guttman. Strand spaces: Proving security protocols correct. Journal of Computer Security,7(2,3):191–230, 1999. 119, 122, 123
Marie-Jeanne Toussaint. Separating the specification and implementation phases in cryptology. In Y. Deswarte, G. Eizenberg, and J.-J. Quisquater, editors, Computer Security-ESORICS 92, pages 77–102. Springer-Verlag, LNCS 648, November 1992. 108
Mark Tuttle. Flaming in Franconia. Remarks made in a panel discussion on the use of formal methods in the analysis of cryptographic protocols at the IEEE Computer Security Foundations Workshop in Franconia, New Hampshire, June 1992. 79
Paul C. van Oorschot. Extending cryptographic logics of belief to key agreement protocols. In Proceedings of the 1st ACM Conference on Computer and Communications Security, pages 233–243. ACM Press, November 1993. 67,76, 85, 88, 95, 98, 126
Gabriele Wedel and Volker Kessler. Formal semantics for authentication logics. In E. Bertino, H. Kurth, G. Martella, and E. Montolivo, editors, Computer Security-ESORICS 96, pages 219–241. Springer-Verlag, LNCS 1146, September 1996. 78, 83, 113, 127
Raphael Yahalom. Optimality of asynchronous two-party secure dataexchange protocol. Journal of Computer Security, 2(2-3):191–209, 1993. 93
Jianying Zhou and Dieter Gollmann. Towards verification of non-repudiation protocols. In T. Vickers J. Grundy, M. Schwenke, editor, International Refinement Workshop and Formal Methods Pacific 1998, pages 370–380. Springer-Verlag, 1998. 127
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Syverson, P., Cervesato, I. (2001). The Logic of Authentication Protocols. In: Focardi, R., Gorrieri, R. (eds) Foundations of Security Analysis and Design. FOSAD 2000. Lecture Notes in Computer Science, vol 2171. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45608-2_2
Download citation
DOI: https://doi.org/10.1007/3-540-45608-2_2
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42896-1
Online ISBN: 978-3-540-45608-7
eBook Packages: Springer Book Archive