University of Birmingham > Talks@bham > Computer Security Seminars > Imposing Order on the Temporal Chaos of ProVerif*

Imposing Order on the Temporal Chaos of ProVerif*

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Vincent Cheval.

(Tom Chothia and Ben Smyth)

Long time security group members may remember a talk by Chris Staite in which he presented an identity management system designed to be used with a cloud service provider that would only perform attacks that could not be detected. I helped Chris develop a protocol for his system that would transfer key material between devices; this protocol is based on Diffie-Hellman with an out of bounds check and a precommitment to avoid a particular kind of brute force attack, and of course I wanted to formally verify this protocol. Modelling the protocol and brute force attack in the applied pi-calculus was easy enough, however checking the protocol in ProVerif was not; ProVerif suggested an impossible, false attack that involved the attacker committing to one value, executing the protocol, learning the values used by the other participants and then going back in time and committing to a different value.

Ben and I focused on proving bound secrecy for the key material (a notion that doesn’t seem to be defined anywhere but is implemented in ProVerif). It was quite easy to prove the protocol correct for a single run by using phase statements to impose order on the process, however we wanted to prove the general case. After many false starts, and some help from Joshua, we worked out that if bound secrecy 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, which can be done with either ProVerif phase statements, or with the StatVerif tool. This provides a general method of checking bound secrecy which avoids many of the false attacks found by ProVerif.

*Ben Smyth does not approve this title.

This talk is part of the Computer Security Seminars series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on talks.cam from the University of Cambridge.