Computer-Aided Security Proofs
Probabilistic programs provide a convenient formalism for defining probability distributions and have numerous applications in computer science. In particular, they are used pervasively in code-based provable security for modeling security properties of cryptographic constructions as well as cryptographic assumptions. Thanks to their well-defined semantics, probabilistic programming languages provide a natural framework to prove the correctness of probabilistic computations. Probabilistic program logics are program logics that allow to reason formally about executions of probabilistic programs, and can be used to verify complex probabilistic algorithms.
- 1.Almeida, J.B., Barbosa, M., Bangerter, E., Barthe, G., Krenn, S., Zanella-Béguelin, S.: Full proof cryptography: verifiable compilation of efficient zero-knowledge protocols. In: ACM Conference on Computer and Communications Security, pp. 488–500. ACM (2012)Google Scholar
- 2.Almeida, J.B., Barbosa, M., Barthe, G., Dupressoir, F.: Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations. Cryptology ePrint Archive, Report 2013/316 (2013)Google Scholar
- 3.Barthe, G., Crespo, J.M., Grégoire, B., Kunz, C., Lakhnech, Y., Schmidt, B., Zanella-Béguelin, S.: Automated analysis and synthesis of padding-based encryption schemes. Cryptology ePrint Archive, Report 2012/695 (2012)Google Scholar
- 5.Barthe, G., Grégoire, B., Zanella-Béguelin, S.: Formal certification of code-based cryptographic proofs. In: 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, pp. 90–101. ACM, New York (2009)Google Scholar
- 6.Barthe, G., Köpf, B., Olmedo, F., Zanella-Béguelin, S.: Probabilistic relational reasoning for differential privacy. In: 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, pp. 97–110. ACM, New York (2012)Google Scholar