Stopping false attacks in ProVerif

ProVerif over-approximates the adversary's power to enable verification of processes under replication. Unfortunately, this results in ProVerif reporting false attacks. This problem is particularly common in protocols whereby a participant commits to a particular value and later reveals their value. We introduce a method to avoid false attacks when analysing secrecy using a compiler that inserts phase statements into a process.

Details can be found in the paper Automatically Checking Commitment Protocols in ProVerif without False Attacks. The examples from this paper can be found below:

Version 1.88 of ProVerif introduced the "otherwise" command for equation definitions, which is used in the last four examples above. If you are using an older version of ProVerif the last four files above will not work, instead you can use these files: the Bluetooth Simple Pairing Protocol & translation, and a simplified pairing protocol & translation.