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: