Computer-Aided Security Proofs for the Working Cryptographer

By Gilles Barthe, Benjamin Gr'egoire, Sylvain Heraud, Santiago Zanella-B'eguelin. Annual International Cryptology Conference, 2011

327 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computer Networks and Communications, Information Systems

View Paper: https://www.semanticscholar.org/paper/e7dbf6c1b47b0956115ff129e0831d99dd07af3c

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computer Networks and Communications

In Information Systems

Citations in the corpus

Probabilistic programming (2014, methodology): “Our prototypical language Prob is imperative, as is the C#-based modeling language underlying Infer.NET [41], and also pWhile, the cryptographic modeling language used by the CertiCrypt [3] and EasyCrypt [4] verification tools for reasoning about cryptographic algorithms and protocols.”
Verified Computational Differential Privacy with Applications to Smart Metering (2013, methodology): “For a detailed description of the semantics of pWHILE we refer the reader to Barthe et al. [5].”
Proving Differential Privacy in Hoare Logic (2014, background): “On a more practical side, it would be interesting to implement our transformation for a realistic setting, for instance modeling thePINQ language [30].”
Probabilistic relational reasoning for differential privacy (2012, methodology): “There are excitingopportunitiesto exploitthe synergies between CertiPriv, CertiCrypt and EasyCrypt, as further discussedinSection8.”
Beyond Differential Privacy: Composition Theorems and Relational Logic for f-divergences between Probabilistic Programs (2013, methodology): “As future work, we intend to implement support for f pRHL in EasyCrypt [4], and formalize the results from [24].”
Relational Reasoning via Probabilistic Coupling (2015, methodology): “In its original form [2], implemented in the EasyCrypt proof assistant [4], pRHL reasons about programs written in a imperative language extended with random assignments with the following syntax of commands:”
Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif (2016, background): “, 2009) and its successor EasyCrypt (Barthe et al., 2011; Barthe et al., 2014b), and CryptoVerif (Blanchet, 2008a).”