The verification of an industrial payment protocol: the SET purchase phase

The Secure Electronic Transaction (SET) protocol has been proposed by a consortium of credit card companies and software corporations to secure e-commerce transactions. When the customer makes a purchase, the SET dual signature guarantees authenticity while keeping the customer's account details secret from the merchant and his choice of goods secret from the bank. This paper reports the first verification results for the complete purchase phase of SET. Using Isabelle and the inductive method, we showed that the credit card details do remain confidential and customer, merchant and bank can confirm most details of a transaction even when some of those details are kept from them. The complex protocol construction makes proofs more difficult but still feasible. Though enough goals can be proved to give confidence in SET, a lack of explicitness in the dual signature makes some agreement properties fail: it is impossible to prove that the customer meant to sent his credit card details to th...