206
8 mars 2018 - 14h00
Automated verification of privacy-type properties for security protocols (MCF Candidate)
par Ivan Gazeau de LORIA, Nancy
Abstract:
The applied pi-calculus is a powerful framework to model protocols and to
define security properties. In this symbolic model, it is possible to
verify automatically complex security properties such as strong secrecy,
anonymity and unlinkability properties which are based on equivalence of processes.
In this talk, we will see an overview of a verification method used by a
tool, Akiss. The tool is able to handle
- a wide range of cryptographic primitives (in particular AKISS is the
only tool able to verify equivalence properties for protocols that use xor);
- protocols with else branches (the treatment of disequalities is often
complicated). We will also provide some insights on how interleaving due to
concurrency can be effectively handled.
