22.03.2013 – Talk by Pedro Adão

Title: Computationally Sound Verification of the NSL Protocol via Computationally Complete Symbolic Attacker
Time: 13:00
Location: Meeting room
Type: Research Result
Speaker: Pedro Adão

We show that the recent technique of computationally complete symbolic attackers  proposed by Bana and Comon-Lundh for computationally sound verification of security protocols is powerful enough to verify actual protocols.  In their work,  Bana and Comon-Lundh presented only the general framework, but they did not introduce sufficiently many axioms to actually prove protocols.We present a  set of  axioms—some generic axioms that are computationally sound for all PPT  algorithms, and two specific axioms that are sound for CCA2 secure encryptions—and illustrate the power of this technique by giving the first computationally sound  verification (secrecy and authentication) via symbolic attackers of the  NSL Protocol  that does not need any further restrictive assumptions about the  computational implementation. These axioms are entirely modular, and not particular to the NSL protocol hence can be reused in the proofs of security for many other security protocols.Joint work with Gergei Bana and Hideki Sakurada