In our paper, we used the formal security analysis tool ProVerif to provide evidence that our suggested protocol is secure. This page contains the ProVerif model files.

• A model of Visa's payWave qVSDC protocol which shows that a wedge attack is possible.
• A model of our new proposed PaySafe protocol.
• A model of our new proposed PaySafe protocol, with the encoding described in our paper which checks for relay attacks.

.