Technical reports

Formal verification of card-holder registration in SET

Giampaolo Bella, Fabio Massacci, Lawrence Paulson, Piero Tramontano

March 2000, 15 pages

DOI: 10.48456/tr-488

Abstract

The first phase of the SET protocol, namely card-holder registration, has been modelled inductively. This phase is presented in outline and its formal model is described. A simple theorem has been proved using Isabelle/HOL, stating that a certification authority will certify a given key at most once. Many ambiguities, contradictions and omissions were noted when formalizing the protocol.

Full text

PDF (1.2 MB)

BibTeX record

@TechReport{UCAM-CL-TR-488,
  author =	 {Bella, Giampaolo and Massacci, Fabio and Paulson, Lawrence
          	  and Tramontano, Piero},
  title = 	 {{Formal verification of card-holder registration in SET}},
  year = 	 2000,
  month = 	 mar,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-488.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-488},
  number = 	 {UCAM-CL-TR-488}
}