Computer-Aided Security Proofs

  • Gilles Barthe
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8054)


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. 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. 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. 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
  4. 4.
    Barthe, G., Grégoire, B., Heraud, S., Béguelin, S.Z.: Computer-aided security proofs for the working cryptographer. In: Rogaway, P. (ed.) CRYPTO 2011. LNCS, vol. 6841, pp. 71–90. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  5. 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. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Gilles Barthe
    • 1
  1. 1.IMDEA Software InstituteSpain

Personalised recommendations