Department of Computer Science and Technology

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


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

  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 = 	 {},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-488},
  number = 	 {UCAM-CL-TR-488}