Verification of security protocols with state in ProVerif : Avoiding false attacks when verifying freshness

Abstract: One of the issues when attempting to verify security properties of a protocol is how to model the protocol. We introduce a method for verifying event freshness in tools which use the applied π-calculus and are able to verify secrecy. Event freshness can be used to prove that a protocol never generates the same key twice. In this work we encode state in the applied π-calculus and perform bounded verification of freshness for MiniDC by using the ProVerif tool. MiniDC is a trivial protocol that for each iteration of a loop generates a unique key and outputs it to a private channel. When verifying freshness, the abstractions of ProVerif cause false attacks. We describe methods which can be used to avoid false attacks that appear when verifying freshness. We show how to avoid some false attacks introduced by private channels, state and protocols that disclose their secret. We conclude that the method used to verify freshness in MiniDCis impractical to use in more complicated protocols with state.