Pitfalls in Formal Reasoning about Security Protocols

Formal verification can give more confidence in the security of cryptographic protocols. Application specific security properties like "The service provider does not loose money" can give even more confidence than standard properties like secrecy or authentication. However, it is surprisingly easy to get a meaningful property slightly wrong. The result is that an insecure protocol can be 'proven' secure. We illustrate the problem with a very small application, a copy card, that has only five different messages. The example is taken from a paper where the protocol is secure, but the proved property slightly wrong. We propose to solve the problem by incorporating more of the real-world application into the formal model.