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.