6th European Symposium on Research in Computer Security (ESORICS 2000)
Formal Verification of Cardholder Registration in SET
Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson, Piero Tramontano
Keywords :
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 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.
(Pages 159-174)