22/06/2012, 16:15 — 17:15 — Room P3.10, Mathematics Building
Gergei Bana, INRIA
Fitting's embedding of first-order logic into first order S4 and
the computationally complete symbolic attacker
We present how first-order logic and a computational semantics
defined via Fitting's embedding of FOL into first-order S4 can be
used to define symbolic attackers of security protocols that are at
least as powerful as the computational ones.