Funded by the EPSRC (October 2000 to October 2003). Grant reference GR/R01156/01. Value £149,442
Security protocols protect messages sent over a network from being read or altered by some enemy. Security protocols often use cryptography and are notoriously error-prone: a fault in the Needham-Schroeder public-key protocol (a trivial one by modern standards) lay undiscovered for over a decade.
Electronic commerce requires protocols of great complexity. To make a purchase over the Internet, the customer typically submits his credit card number to the merchant, protected by a protocol such as SSL. However, many potential customers are uneasy about revealing their credit card number over the Internet. The SET protocol [13,14,15] has been proposed by a consortium of credit card and software companies. SET aims to protect sensitive card-holder information, to ensure payment integrity and to authenticate merchants and card-holders.
The overall architecture of SET is based on a rooted hierarchy of Certification Authorities (CAs), whose task is to provide customers with digital certificates for signature and encryption. Customers must generate and safeguard their private keys. A normal run of the SET protocol consists of five phases. The first two phases — Card-holder Registration and Merchant Registration — are used by the protocol participants to register their keys and to get the appropriate certificates. The remaining three phases — Purchase Request, Payment Authorization and Payment Capture — constitute the electronic transaction itself. To accomplish these tasks SET uses numerous combinations of hashing, public key and symmetric key cryptography based on the PKCS#7 standards from RSA Laboratories [12].
SET has been deployed, for example, in Microsoft Wallet. Companies such as Hitachi, IBM and VeriSign are currently testing SET-based products. Some security experts feel that, for various reasons, SET will never gain widespread acceptance. Whether it does or not, we can be certain that new e-commerce protocols will be developed. Unlike SSL, they will not require the customer to trust the merchant. These new protocols will probably share much of SET's architecture, as outlined in the previous paragraph.
Many researchers have looked at the problem of verifying e-commerce protocols, but much work remains to be done. Here are a few examples from the extensive literature. Brackin [5] analyzed two Cybercash protocols. His method `addresses only parts of the protocol failure problem, but addresses these parts quickly and automatically.' Bolignano [4] described (in 1997) an approach combining the Coq tool with a translation of properties into finite automata; he claimed to be working on SET, but no results have been published. Kessler and Neumann [6] have designed a belief logic to analyse a single message of the payment phase of SET. These efforts are valuable, but in each case the formal model is very abstract, allowing obvious flaws to go undetected. The last two approaches rely on authentication logics, which have been known to deliver misleading results. Model-checking is a more reliable verification method; a recent example is the analysis by Shmatikov and Mitchell [16] of a contract signing protocol.
With previous EPSRC funding, the principal investigator has developed an inductive method for analyzing cryptographic protocols [9]. The method is built on simple foundations: an operational semantics of a system consisting of good agents, a bad agent, and trusted servers. It can easily be extended to model new hardware, such as smart cards. Properties are proved using Isabelle [8]. Although the proofs are not automatic, an expert user can analyze a protocol in days or weeks. Important protocols have been analyzed, such as Kerberos IV [3].
The objective of the proposed project is to conduct an inductive analysis of some e-commerce protocols, including SET. An inductive analysis of SSL (or rather of TLS as it is now called) has already been undertaken [10]. Preliminary experiments suggest that even SET can be analyzed, but it will be a much greater task. Some colleagues and I [2] have formalized the first phase of SET, namely Card-holder Registration, and proved a simple fact about it. Given enough time and resources, a more thorough analysis of SET should be possible.
SET is complicated: its documentation [13,14,15] totals nearly 1000 pages. The project will identify and analyze those elements of SET that are of scientific interest. As usual with formal methods, we shall not be concerned with bit-level details, and whenever possible we shall regard cryptographic primitives as black boxes. By focussing on the top-level architecture, we expect our analysis to be relevant to other e-commerce protocols.
The programme of work will consist of proceeding through the five phases of SET, one after the other. In this first pass, in order to avoid getting bogged down, we shall prove only the more straightforward properties, while identifying deeper properties to be proved in a second pass. Straightforward properties include integrity of messages. Deeper properties include confidentiality and authenticity.
The analysis of SET will mainly be carried out by the research assistant, with the assistance of the principal investigator (Paulson). We expect to collaborate with Dr. Fabio Massacci of the University of Siena, Italy. Dr. Massacci played a major role in the preliminary analysis of SET's Card-holder Registration phase.
A natural by-product of these proofs will be to extend the existing protocol verification environment with new theories and proof methods tailored to the cryptographic primitives used in SET. This extended environment will be valuable in its own right, and we shall apply it to other protocols.
While the SET analysis is under way, we shall look out for other e-commerce protocols to verify. New ones are regularly published in conferences such as Security and Privacy (Oakland) and Financial Cryptography, though only the most significant protocols can be verified in the time available. They are typically quite simple and could be analyzed by either the research assistant or the principal investigator. They may offer facilities not available in SET, such as micro-payments or non-repudiation.
Paulson will direct the project and will maintain and extend Isabelle. He will develop formal models of the protocols in conjunction with the research assistant.