The secure electronic transaction (SET) standard specifies a sophisticated protocol, aimed at securing e-commerce transactions. It improves on secure sockets layer (SSL), which merely focuses on preventing eavesdropping, by focusing on possible untrustworthy agents in a transaction: merchants who might misuse or not properly guard credit card information, and customers who may not be who they say they are. The difficulty with the SET protocol is its size and complexity: documentation requiring over 1,000 pages, many levels of encryption, numerous messages during a transaction, and multiple alternative protocol paths. As with any complex system, the question is simply: Will it work as advertised?

Like Bella et al. [1], the authors of this work focus on the formal verification of a reasonably simplified version of the SET payment protocol (just one part of the larger overall protocol). The approach is to use observational transition system (OTS)/CafeOBJ, the latter of which is an algebraic specification language in which an OTS can be specified as a collection of rewriting rules. The authors prove that the simplified protocol is secure against attack by intruders, and appropriately hides information from both customers and merchants. The paper provides enough detail for the reader to get a good sense of the approach, but a complete discussion would go far beyond what is possible in a brief paper.

A limitation of the paper is that, unlike Bella et al. [1], the authors give readers little in the way of background about SET, and plunge into detail without sufficient general discussion. Still, all in all, this work is an important application of formal methods to protocol verification.