Abstract
The first phase of the SET protocol, namely Cardholder Registration, has been modelled inductively. This phase is presented in outline and its formal model is described. A number of basic lemmas have been proved about the protocol using Isabelle/HOL, along with a theorem stating that a certification authority will certify a given key at most once. Many ambiguities, contradictions and omissions were noted while formalizing the protocol.
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
Bella, G.: Message reception in the inductive approach. Research Report 460, University of Cambridge – Computer Laboratory (1999)
Bella, G.: Modelling agents’ knowledge inductively. In: Malcolm, J.A., Christianson, B., Crispo, B., Roe, M. (eds.) Security Protocols 1999. LNCS, vol. 1796. Springer, Heidelberg (2000)
Bella, G., Paulson, L.C.: Kerberos version IV: Inductive analysis of the secrecy goals. In: Quisquater, J.-J., Deswarte, Y., Meadows, C., Gollmann, D. (eds.) ESORICS 1998. LNCS, vol. 1485, pp. 361–375. Springer, Heidelberg (1998)
Brackin, S.: Automatic formal analyses of two large commercial protocols. In: Proceedings of the DIMACS Workshop on Design and Formal Verification of Security Protocols (September 1997), Available on the web at http://www.arca.com/proj_papers/brackin/dimacs.pdf
Brackin, S.: Automatically detecting authentication limitations in commercial security protocols. In: Proceedings of the 22nd National Conference on Information Systems Security (October 1999), Available on the web at http://www.arca.com/proj_papers/brackin/Nissc99.pdf
CCITT. Recommendation X.509: The Directory - Authentication Framework (1988), Available electronically at http://www.itu.int/itudoc/itu-t/rec/x/x500up/x509.html
Kailar, R.: Reasoning about accountability in protocols for electronic commerce. In: Proc. of the 14th IEEE Sym. on Sec. and Privacy, pp. 236–250. IEEE Computer Society Press, Los Alamitos (1995)
Kessler, V., Neumann, H.: A sound logic for analysing electronic commerce protocols. In: Quisquater, J.-J., Deswarte, Y., Meadows, C., Gollmann, D. (eds.) ESORICS 1998. LNCS, vol. 1485, pp. 345–360. Springer, Heidelberg (1998)
Loeb, L.: Secure Electronic Transactions: Introduction and Technical Reference. Computer Science. Artech House 1998, Enclosed a CD-ROM with SET Reference Implementation Version 1.0
Lowe, G.: A hierarchy of authentication specifications. In: Proc. of the 10th IEEE Comp. Sec. Found. Workshop, pp. 31–43. IEEE Computer Society Press, Los Alamitos (1997)
Mastercard & VISA. SET Secure Electronic Transaction Specification: Business Description (May 1997), Available electronically at http://www.setco.org/set_specifications.html
Mastercard & VISA. SET Secure Electronic Transaction Specification: Formal Protocol Definition (May 1997), Available electronically at http://www.setco.org/set_specifications.html
Mastercard & VISA. SET Secure Electronic Transaction Specification: Programmer’s Guide (May 1997), Available electronically at http://www.setco.org/set_specifications.html
Meadows, C.: Open issues in formal methods for cryptographic protocol analysis. In: Proceedings of DISCEX 2000, pp. 237–250. IEEE Comp. Society Press, Los Alamitos (2000)
Meadows, C., Syverson, P.: A formal specification of requirements for payment transactions in the SET protocol. In: Hirschfeld, R. (ed.) FC 1998. LNCS, vol. 1465, pp. 122–140. Springer, Heidelberg (1998)
Needham, R.M., Schroeder, M.: Using encryption for authentication in large networks of computers. Comm. of the ACM 21(12), 993–999 (1978)
O’Mahony, D., Peirce, M., Tewari, H.: Electronic payment systems. The Artech House computer science library. Artech House (1997)
Paulson, L.C.: The inductive approach to verifying cryptographic protocols. J. of Comp. Sec. 6, 85–128 (1998)
Paulson, L.C.: Inductive analysis of the internet protocol TLS. ACM Trans. on Inform. and Sys. Sec. 2(3), 332–351 (1999)
RSA Laboratories. PKCS-6: Extended-Certificate Syntax Standard (1993), Available electronically at http://www.rsasecurity.com/rsalabs/pkcs
RSA Laboratories. PKCS-7: Cryptographic Message Syntax Standard (1993), Available electronically at http://www.rsasecurity.com/rsalabs/pkcs
Schneider, S.: Verifying authentication protocols in CSP. IEEE Trans. on Software Engineering 24(9), 741–758 (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bella, G., Massacci, F., Paulson, L.C., Tramontano, P. (2000). Formal Verification of Cardholder Registration in SET. In: Cuppens, F., Deswarte, Y., Gollmann, D., Waidner, M. (eds) Computer Security - ESORICS 2000. ESORICS 2000. Lecture Notes in Computer Science, vol 1895. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10722599_10
Download citation
DOI: https://doi.org/10.1007/10722599_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41031-7
Online ISBN: 978-3-540-45299-7
eBook Packages: Springer Book Archive