An overview of the verification of SET

This paper describes the verification of Secure Electronic Transaction (SET), an e-commerce protocol by VISA and MasterCard. The main tasks are to comprehend the written documentation, to produce an accurate formal model, to identify specific protocol goals, and, finally, to prove them. The main obstacles are the protocol's complexity (due in part to its use of digital envelopes) and its unusual goals involving partial information sharing. Our verification efforts show that the protocol does not completely satisfy its goals, although the flaws are minor. The primary outcome of the project is experience with verification of enormous and complicated protocols. This paper summarizes the project - the details appear elsewhere [11 - 13] - focusing on the issues and the conclusions. © Springer-Verlag 2005.