Author: 

Tom Clothia

Title: 

Helping ProVerif Get Over Its Commitment Issues

Abstract:

The ProVerif tool can prove secrecy for an unbounded number of runs of
a protocol. However, to do this ProVerif has to make some abstractions
that might lead it to claim a false attack in a correct protocol. In
particular, in protocols where one principal commits to a value, and
then later releases that value, ProVerif normally finds a false
attack. We present a method of avoiding these false attacks by
defining secrecy for bound names and showing that if this fails then
there is a single point of failure, i.e., it is enough to verify one
copy of the protocol with the secret value in parallel with a infinite
number of copies of the protocol with a dummy value. The false attacks
can then be removed, and semantic correctness preserved, by imposing
order on just the single copy of the protocol that uses the secret
value. This provides a general method of checking bound secrecy which
avoids many of the false attacks found by ProVerif.