Description
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.
Prochains exposés
-
The Design and Implementation of a Virtual Firmware Monitor
Orateur : Charly Castes - EPFL
Low level software is often granted high privilege, yet this need not be the case. Although vendor firmware plays a critical role in the operation and management of the machine, most of its functionality does not require unfettered access to security critical software and data. In this paper we demonstrate that vendor firmware can be safely and efficiently deprivileged, decoupling its[…]-
SoSysec
-
Compartmentalization
-
Operating system and virtualization
-