@inproceedings{gregoire2012probabilistic,
author = {Gregoire, Benjamin and Strub, Pierre-Yves and Swamy, Nikhil and Zanella-Béguelin, Santiago and Barthe, Gilles and Fournet, Cédric},
title = {Probabilistic Relational Verification for Cryptographic Implementations},
year = {2012},
month = {November},
abstract = {In the form of tools like EasyCrypt, relational program logics have been used for mechanizing formal proofs of various cryptographic constructions. With an eye towards scaling these successes towards end-to-end security proofs for implementations of distributed systems, we present rF*, a new extension of F*, a general-purpose higher-order stateful programming language with a verification system based on refinement types.

The distinguishing feature of rF* is a new probabilistic, relational Hoare logic, formalized in Coq---the first such logic for a higher-order, stateful language. We prove the soundness of this logic against a new denotational semantics for rF*, in contrast to prior operational formalizations of F*. Through careful language design, we adapt the F* typechecker to generate both classic and relational verification conditions, and to automatically discharge their proofs using an SMT solver. Thus, we are able to benefit from the existing features of F*, including, for example, its abstraction facilities that support modular reasoning about program fragments. We evaluate rF* experimentally by programming a series of cryptographic constructions and protocols, and by verifying their security properties, ranging from information flow to unlinkability, integrity, and privacy.},
url = {http://approjects.co.za/?big=en-us/research/publication/probabilistic-relational-verification-for-cryptographic-implementations/},
}