Ebook Verifying the SET Purchase Protocols
SET (Secure Electronic Transaction) is a huge suite of protocols devised by Visa and Mastercard for on-line shopping. In this paper, we focus on the purchase phase of SET and its key construct: the dual signature. This mechanism lets the customer agree the order details with the merchant while hiding those details from the bank; at the same time, it lets the customer share his credit card details with the bank while hiding them from the merchant.
We are looking at SET because within it are ideas of scientific interest for security verification and security protocol design. For example, PKCS digital envelopes will be used in future protocols whether or not SET is a commercial success. Moreover, its sheer size, over 1000 pages of official documentation makes it a challenge for formal verification.
We have carefully simplified SET to make its analysis tractable, but we have retained the most important mechanisms. Our simplified version of SET is still one of the most complex protocols ever to be analysed formally.
We have found that, on the whole, dual signatures seem to work: the credit card details do remain confidential and still the various parties can be sure that they are dealing with the same transaction, even if they possess only partial information. Unfortunately, the dual signature, in common with many other SET messages, violates the explicitness principle of Abadi and Needham. So some guarantees are weaker than they should be particularly for the Payment Gateway, whose function is to authorize transactions.
In other papers, we have described modelling issues of the general SET protocol. The present paper describes work on verifying SET’s Purchase phases using the inductive method and the Isabelle theorem prover.
Paper outline. In the next sections we present an overview of SET (§2) and of its purchase phase (§3). We discuss the formal model, presenting the most complicated rule using Isabelle syntax (§4). Then we discuss the proofs (§5) and conclude with a brief discussion of related work (§6).
Contents
1 Introduction
2 SET Overview
3 The SET Purchase Protocols
4 The Formal Model
5 The Proofs
6 Related Work and Conclusions
Posted in :
