Section: New Results

Computationally Complete Symbolic Attacker Models

Participants : Gergei Bana, Hubert Comon-Lundh [ENS Cachan] , Rohit Chadha [University of Missouri] .

In previous work, Bana and Comon-Lunch proposed a new approach to computational verification of cryptographic protocols, by defining a computationally complete symbolic attacker, so that a symbolic proof against this attacker can be shown to imply a computational proof of security  [27] , [28] .

Following on from this work, Bana and Chadha fully developed the core parts of the computationally complete symbolic attacker based on indistinguishability. This covers both trace properties and equivalence properties and can be proved partially complete. They evaluated their method by applying it to several classic protocols. This work is currently under submission.

Bana, Comon-Lundh, and Koutsos also worked on a decision procedure for the computationally complete symbolic attacker based on indistinguishability.