Abstract
We present the adaptation of our model for the validation of key distribution and authentication protocols to address specific needs of protocols for electronic commerce. The two models defer in both the threat scenario and in the formalization. We demonstrate the suitability of our adaptation by analyzing a specific version of the Internet Billing Server protocol introduced by Carnegie Mellon University. Our analysis shows that, while the security properties a key distribution or authentication protocol shall provide are well understood, it is often not clear what properties an electronic commerce protocol can or shall provide. Our methods rely on automatic theorem proving tools. Specifically, we used “Otter”, an automatic theorem proving software developed at Argonne National Laboratories.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
G. Bella and L.C. Paulson. Kerberos version iv: Inductive analysis of the secrecy goals. In 5th European Symposium on Research in Computer Security, Lecture Notes in Computer Science, pages 361–375. Springer-Verlag, 1998.
M. Bellare, R. Canetti, and H. Krawczyk. A Modular Approach to the Design and Analysis of Authentication and Key Exchange Protocols. In Annual Symposium on the Theory of Computing. ACM, 1998.
M. Bellare and P. Rogaway. Provably secure session key distribution-the three party case. In Annual Symposium on the Theory of Computing, pages 57–66. ACM, 1995.
R. Berger, S. Kannan, and R. Peralta. A framework for the study of cryptographic protocols. In Advances in Cryptology-CRYPTO ’95, Lecture Notes in Computer Science, pages 87–103. Springer-Verlag, 1985.
S. Brackin. Automatically detecting authentication limitations in commercial security protocols. In Proc. of the 22nd National Conference on Information Systems Security, October 1999.
M. Burrows, M. Abadi, and R. Needham. A Logic of Authentication. Report 39, Digital Systems Research Center, Palo Alto, California, Feb 1989.
D. Denning and G. Sacco. Timestamps in key distribution protocols. Communications of the ACM, 24:533–536, 1982.
DIN NI-17.4. Spezifikation der Schnittstelle zu Chipkarten mit Digitaler Signatur-Anwendung / Funktion nach SigG und SigV, Version 1.0 (Draft), November 1998.
D. Dolev and A. Yao. On the security of public-key protocols. IEEE Transactions on Information Theory, 29:198–208, 1983.
S. Gürgens and R. Peralta. Efficient Automated Testing of Cryptographic Protocols. Technical report, GMD German National Research Center for Information Technology, 1998.
N. Heintze and J.D. Tygar. A Model for Secure Protocols and their Compositions. In 1994 IEEE Computer Society Symposium on Research in Security and Privacy, pages 2–13. IEEE Computer Society Press, May 1994.
R. Kailar. Accountability in Electronic Commerce Protocols. In IEEE Transactions on Software Engineering, volume 22, pages 313–328. IEEE, 1996.
G. Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using CSP and FDR. In Second International Workshop, TACAS ’96, volume 1055 of LNCS, pages 147–166. SV, 1996.
W. Marrero, E. M. Clarke, and S. Jha. A Model Checker for Authentication Protocols. In DIMACS Workshop on Cryptographic Protocol Design and Verification, http://dimacs.rutgers.edu/Workshops/Security/, 1997.
C. Meadows. A system for the specification and verification of key management protocols. In IEEE Symposium on Security and Privacy, pages 182–195. IEEE Computer Society Press, New York, 1991.
C. Meadows. Formal Verification of Cryptographic Protocols: A Survey. In Advances in Cryptology-Asiacrypt ’94, volume 917 of LNCS, pages 133–150. SV, 1995.
C. Meadows. Analyzing the Needham-Schroeder Public Key Protocol: A Comparison of Two Approaches. In Proceedings of ESORICS, Naval Research Laboratory, 1996. Springer.
C. Meadows and P. Syverson. A formal specification of requirements for payment transactions in the SET protocol. In Proceedings of Financial Cryptography, 1998.
R. Needham and M. Schroeder. Using encryption for authentication in large networks of computers. Communications of the ACM, pages 993–999, 1978.
R. Ostrovsky and M. Yung. How to withstand mobile virus attacks. In Proceedings of PODC, pages 51–59, 1991.
K. O’Toole. The Internet Billing Server-Transaction Protocol Alternatives. Technical Report INI TR 1994-1, Carnegie Mellon University, Information Networking Institute, 1994.
L. C. Paulson. The inductive approach to verifying cryptographic protocols. Journal of Computer Security, 6:85–128, 1998.
L. C. Paulson. Inductive Analysis of the Internet Protocol TLS. ACM Trans. on Information and System Security, 2(3):332–351, 1999.
R. L. Rivest, A. Shamir, and L. A. Adleman. A method for obtaining digital signatures and public-key cryptosystems. Communications of the ACM, 21(2):120–126, 1978.
B. Roscoe, P. Ryan, S. Schneider, M. Goldsmith, and G. Lowe. The modelling and Analysis of Security Protocols. Addison Wesley, 2000.
C. Rudolph. A Formal Model for Systematic Design of Key Establishment Protocols. In Information Security and Privacy (ACISP 98), Lecture Notes in Computer Science. Springer Verlag, 1998.
S. Schneider. Verifying authentication protocols with CSP. In IEEE Computer Security Foundations Workshop. IEEE, 1997.
V. Shoup and A. Rubin. Session key distribution using smart card. In Advances in Cryptology-EUROCRYPT ’96, volume 1070 of LNCS, pages 321–331. SV, 1996.
M. Tatebayashi, N. Matsuzaki, and D. Newman. Key Distribution Protocol for Digital Mobile Communication Systems. In G. Brassard, editor, Advances in Cryptology-CRYPTO ’89, volume 435 of LNCS, pages 324–333. SV, 1991.
L. Wos, R. Overbeek, E. Lusk, and J. Boyle. Automated Reasoning-Introduction and Applications. McGraw-Hill, Inc., 1992.
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
Gürgens, S., Lopez, J. (2001). Suitability of a Classical Analysis Method for E-commerce Protocols. In: Davida, G.I., Frankel, Y. (eds) Information Security. ISC 2001. Lecture Notes in Computer Science, vol 2200. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45439-X_4
Download citation
DOI: https://doi.org/10.1007/3-540-45439-X_4
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42662-2
Online ISBN: 978-3-540-45439-7
eBook Packages: Springer Book Archive