Automatic verification of security in payment protocols for electronic commerce

In order to make secure transactions over computer networks, various cryptographic protocols have been proposed but, because of subtleties involved in their design, many of them have been shown to have flaws, even a long time after their publication. For this reason, several automatic verification methods for analyzing these protocols have been devised. The aim of this paper is to present a methodology for verifying security requirements of electronic payment protocols by means of NuSMV, a symbolic model checker. Our work principally focus on formal representation of security requirements. Indeed, we propose an extension of the correspondence property, so far used only for authentication, to other requirements as confidentiality and integrity. These are the basic security requirements of payment protocols for electronic commerce. We illustrate as case study a variant of the SET protocol proposed by Lu & Smolka. This variant has been formally verified by Ly & Smolka and considered secure. Conversely, we have discovered two attacks that allow a dishonest user to purchase a good debiting the amount to another user.