Computer Laboratory

Technical reports

Verifying the SET registration protocols

Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson

March 2002, 24 pages

Abstract

SET (Secure Electronic Transaction) is an immense e-commerce protocol designed to improve the security of credit card purchases. In this paper we focus on the initial bootstrapping phases of SET, whose objective is the registration of customers and merchants with a SET certification authority. The aim of registration is twofold: getting the approval of the cardholder’s or merchant’s bank, and replacing traditional credit card numbers with electronic credentials that customers can present to the merchant, so that their privacy is protected. These registration sub-protocols present a number of challenges to current formal verification methods. First, they do not assume that each agent knows the public keys of the other agents. Key distribution is one of the protocols’ tasks. Second, SET uses complex encryption primitives (digital envelopes) which introduce dependency chains: the loss of one secret key can lead to potentially unlimited losses. Building upon our previous work, we have been able to model and formally verify SET’s registration with the inductive method in Isabelle/HOL solving its challenges with very general techniques.

Full text

PDF (0.4 MB)

BibTeX record

@TechReport{UCAM-CL-TR-531,
  author =	 {Bella, Giampaolo and Massacci, Fabio and Paulson, Lawrence
          	  C.},
  title = 	 {{Verifying the SET registration protocols}},
  year = 	 2002,
  month = 	 mar,
  url = 	 {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-531.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-531}
}