Reference from ESORICS proceedings

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)

Proceedings table of contents