Abstract
The security of electronic communication relies to a great extent on the security of authentication protocols used to distribute cryptographic keys. Hence formal techniques are needed which help to analyse the security of these protocols. In this paper we introduce a formal method which allows to detect the possibility of certain replay and interleaving attacks. By using our method we are able to show the weakness of the Neuman-Stubblebine protocol and to detect inaccuracies in some authentication protocols standardized in ISO. These inaccuracies may cause the protocol to allow interleaving attacks in certain environments, a fact which seems to be unrecognized so far.
Funded by Deutsche Telekom AG, Darmstadt
Preview
Unable to display preview. Download preview PDF.
References
Abadi, M., Tuttle, MR.: A Semantics for a Logic of Authentication. Proceedings of the Tenth Annual ACM Symposium on Principles of Distributed Computing, Montreal, Canada, August 1991, pp. 201–216.
Burrows, M., Abadi, M., Needham, R.: A Logic of Authentication. Report 39 Digital Systems Research Center, Palo Alto, California, 1989.
Carlsen, U.: Using Logics to Detect Implementation-Dependent Flaws. Ninth Annual Computer Security Applications Conference, De. 6-10, 1993, Orlando, Florida, pp. 64–73.
CCITT Recommandation X.509-ISO/IEC 9594/8 (1987)
Denning, D.E., Sacco, G.M.: Timestamps in Key Distribution Protocols. CALM Vol. 24, No. 8, August 1982, pp. 533–536.
ElGamal, T.,: A Public Key Cryptosystem and a Signature Scheme based on Discrete Logarithms, IEEE Transactions on Information Theory, Vol.31, NrA, July 1985, S.469–472
Gaarder, K., Snekkenes, E.: Applying a Formal Analysis Technique to the CCITT X.509 Strong Two-Way Authentication Protocol. J. Cryptology, Vol. 3, No. 2 (1991) 81–98.
Gong, L., Needham, R., Yahalom, R.: Reasoning about Belief in Cryptographic Protocols. Proc. 1990 IEEE Symp. on Security and Privacy (Oakland, California), pp. 234–248.
Güergens, S.: A Formal Analysis Technique for Authentication Protocols. Proceedings of Pragocrypt 1996.
ISO/IEC 7816-4: 1995(E) “Information technology-Identification cards-Integrated circuit(s) cards with contacts-Part 4: Inter-industry commands for interchange”
WD 7816-8: 1995(E) “Information technology-Identification cards-Integrated circuit(s) cards with contacts-Part 8: Security related interindustry commandsx”
ISO/IEC 9798-2: 1994(E) “Information technology-Security techniques-Entity authentication-Part 2: Mechanisms using encipherment algorithms”
Mathuria, A., Safavi-Naini, R, Nickolas, P.: Some Remarks on the Logic of Gong, Needham and Yahalom. Proceedings of the International Computer Symposium 1994, Dec. 12-15, NCTU, Hsinchu, Taiwan, R.O.C, Vol.1, pp. 303–308
Needham, R. M., Schroeder, M. D.: Authentication Revisited. Operating Systems Review, Vol. 21, No. 12, December 1978, pp. 993–999.
Neuman, B.C., Stubblebine, S.G.: A note on the use of timestamps as Nonces. Operating Systems Rev. 27 (2), 1993, pp. 10–14.
Rivest, R. L., Shamir, A., Adleman, L. A.: A method for obtaining digital signatures and public-key cryptosystems; Communications of the ACM, Vol.21, Nr.2, 1978, 5.120-126.
Syverson, P.: On Key Distribution Protocols for Repeated Authentication; Operating Systems Review, vol. 27, no. 4, October 1993, pp. 24–30.
Van Oorschot, P.C.: Extending Cryptographic Logics of Belief to Key Agreement Protocols. 1st ACM Conference on Computer and Communications Security, Nov. 3-5 1993, Fairfax, Virginia, pp. 232–243.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gürgens, S. (1998). SG logic — a formal analysis technique for authentication protocols. In: Christianson, B., Crispo, B., Lomas, M., Roe, M. (eds) Security Protocols. Security Protocols 1997. Lecture Notes in Computer Science, vol 1361. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0028167
Download citation
DOI: https://doi.org/10.1007/BFb0028167
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64040-0
Online ISBN: 978-3-540-69688-9
eBook Packages: Springer Book Archive