Verification of Security Properties in Electronic Payment Protocols

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. For instance, these are the basic security requirements of electronic payment protocols as SET. We illustrate as case study a variant of SET proposed by Lu and Smolka. This variant has been proposed in order to obtain a version of protocol more suitable for formal analysis. Notice that, up to now this variant has been considered secure