5 papers
The Last Mile: High-Assurance and High-Speed Cryptographic Implementations
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe +5
We develop a new approach for building cryptographic implementations. Our approach goes the last mile and delivers assembly code that is provably functionally correct, protected ag…
Deciding Indistinguishability
Adrien Koutsos
Computational indistinguishability is a key property in cryptography and verification of security protocols. Current tools for proving it rely on cryptographic game transformations…
The 5G-AKA Authentication Protocol Privacy
Adrien Koutsos
We study the 5G-AKA authentication protocol described in the 5G mobile communication standards. This version of AKA tries to achieve a better privacy than the 3G and 4G versions th…
A Sound Flow-Sensitive Heap Abstraction for the Static Analysis of Android Applications
Stefano Calzavara, Ilya Grishchenko, Adrien Koutsos +1
The present paper proposes the first static analysis for Android applications which is both flow-sensitive on the heap abstraction and provably sound with respect to a rich formal…
Formal Computational Unlinkability Proofs of RFID Protocols
Hubert Comon, Adrien Koutsos
We set up a framework for the formal proofs of RFID protocols in the computational model. We rely on the so-called computationally complete symbolic attacker model. Our contributio…