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, pp.97-110

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

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

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

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