From Computationally-proved Protocol Specifications to Implementations. - David Cadé; Bruno Blanchet (ARES, 2012)

From Computationally-Proved Protocol Specifications to Implementations and Application to SSH. - David Cadé; Bruno Blanchet (J. Wirel. Mob. Networks Ubiquitous Comput. Dependable Appl., 2013)

Proved Implementations of Cryptographic Protocols in the Computational Model. (Implémentations de protocoles cryptographiques prouvées dans le modèle calculatoire). - David Cadé (2013)

Proved generation of implementations from computationally secure protocol specifications. - David Cadé; Bruno Blanchet (J. Comput. Secur., 2015)