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.
Next sessions
-
A non-comparison oblivious sort and its application to private k-NN
Speaker : Sofiane Azogagh - UQÀM
Sorting is a fundamental subroutine of many algorithms and as such has been studied for decades. A well-known result is the Lower Bound Theorem, which states that no comparison-based sorting algorithm can do better than O(nlog(n)) in the worst case. However, in the fifties, new sorting algorithms that do not rely on comparisons were introduced such as counting sort, which can run in linear time[…]-
Cryptography
-
SoSysec
-
Privacy
-
Databases
-
Secure storage
-