Formal verification of card-holder registration in SET
Giampaolo Bella, Fabio Massacci, Lawrence Charles Paulson, Piero Tramontano · 2021
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.