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.
