Technical reports
Verifying the SET registration protocols
Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson
March 2002, 24 pages
DOI: 10.48456/tr-531
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 = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-531.pdf}, institution = {University of Cambridge, Computer Laboratory}, doi = {10.48456/tr-531}, number = {UCAM-CL-TR-531} }