Using ENDL to verify Cardholder Registration in SET Protocol

Abstract

Secure electronic commerce relies on the application of secure transaction protocol. However, even with the so-called secure protocol, the communication can be compromised frequently without effective approach to detect the subtle flaws before it launches into practice. We generated ENDL[2] that is used to formally verify the authentication properties of secure transaction protocols. We have showed how to employ it to depict the complicated security properties of secure protocols, especially the instances in SET (Secure Electronic Transaction) protocol, in our previous work [3]. The first stage of the SET protocol, namely Cardholder Registration, has been defined in book [1] respectively. It formally describes the seven fundamental steps of the flow of transactions in outline. Based on the ENDL, we describe the whole verification of cardholder registration process in this paper. Some potentially dangerous flaws of SET protocol are noted while verifying the protocol.