The Modelling and Analysis of Security Protocols: the CSP Approach

C.1. Secrecy

We first consider the secrecy property required of this protocol. Some details of the transaction (such as its value) are available to eavesdroppers in the original protocol, and hence are not required to be kept secret. However, some care is taken to keep the card number secret, and we will take this as the secrecy property that is required for the protocol: that if the customer interacts with an honest merchant then the intruder cannot learn cardNumber. (Clearly if the customer interacts with a dishonest merchant or the intruder posing as a merchant then no guarantees can be expected concerning secrecy of the card number.)

We will provide a rank function that demonstrates that the protocol indeed satisfies this property. To do ...