G. Barthe, B. Grégoire, S. Heraud, and S. Z. Béguelin, Computer-Aided Security Proofs for the Working Cryptographer, Advances in Cryptology ? CRYPTO 2011, pp.71-90, 2011.
DOI : 10.1007/978-3-642-22792-9_5

URL : https://hal.archives-ouvertes.fr/hal-01112075

G. Barthe, B. Grégoire, and S. Z. Béguelin, Formal certification of code-based cryptographic proofs, 36th ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages, pp.90-101, 2009.

G. Barthe, B. Köpf, F. Olmedo, and S. Z. Béguelin, Probabilistic reasoning for differential privacy, 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, 2012.

M. Bellare and P. Rogaway, Random oracles are practical, Proceedings of the 1st ACM conference on Computer and communications security , CCS '93, pp.62-73, 1993.
DOI : 10.1145/168588.168596

M. Bellare and P. Rogaway, The Security of Triple Encryption and a Framework??for??Code-Based??Game-Playing??Proofs, Advances in Cryptology ? EURO- CRYPT 2006, pp.409-426, 2006.
DOI : 10.1007/11761679_25

N. Benton, Simple relational correctness proofs for static analyses and program transformations, 31st ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages, pp.14-25, 2004.

Y. Deng and W. Du, Logical, metric, and algorithmic characterisations of probabilistic bisimulation, 2011.

J. Desharnais, F. Laviolette, and M. Tracol, Approximate Analysis of Probabilistic Processes: Logic, Simulation and Games, 2008 Fifth International Conference on Quantitative Evaluation of Systems, pp.264-273, 2008.
DOI : 10.1109/QEST.2008.42

C. Dwork, Differential Privacy, 33rd International Colloquium on Automata , Languages and Programming, pp.1-12, 2006.
DOI : 10.1007/11787006_1

S. Goldwasser and S. Micali, Probabilistic encryption, Journal of Computer and System Sciences, vol.28, issue.2, pp.270-299, 1984.
DOI : 10.1016/0022-0000(84)90070-9

S. Halevi, A plausible approach to computer-aided cryptographic proofs, Cryptology ePrint Archive Report, vol.181, 2005.

B. Jonsson, W. Yi, and K. G. Larsen, Probabilistic extensions of process algebras, Handbook of Process Algebra, pp.685-710, 2001.

R. Segala and A. Turrini, Approximated Computationally Bounded Simulation Relations for Probabilistic Automata, 20th IEEE Computer Security Foundations Symposium (CSF'07), pp.140-156, 2007.
DOI : 10.1109/CSF.2007.8