Thursday 20 July 2017, LSV, 10:00: A complete and terminating strategy for the Bana-Comon equivalence logic, Adrien Koutsos (LSV).
The Bana-Comon logic (also known as the Complete Symbolic
Attacker Model) is a first-order logic used to prove computational
equivalence of security protocols. It has only one (binary) predicate,
which expresses the fact that two messages are indistinguishable, for
any adversary with reasonable computing capabilities. This logic has
several advantages compared to the standard approaches used to
formally prove security protocols, e.g. it offers strong security
guarantees and makes explicit all implementation assumptions.
The BC logic was successfully used to prove security of protocols by hand, but the proof are hard to read, and there is still a risk of mistakes. We therefore developed a complete and terminating strategy allowing to do automatic machine checked proofs (for a fragment of the logic). I will present the key difficulties and ideas allowing to decide a fragment of the logic, hence the security of protocols.