ask others

Benjamin Grégoire

> Home > Persons

Refine list

refinements active!

zoomed in on ?? of ?? records

view refined list in

showing all ?? records

2010 – today

see FAQ

What is the meaning of the colors in the publication lists?

2018
[j4]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - journals/pacmpl/BartheEGHS18
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/pacmpl/BartheEGHS18
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Proving expected sensitivity of probabilistic programs. PACMPL 2(POPL): 57:1-57:29 (2018)
[c61]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/ccs/BartheFGGJS18
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/ccs/BartheFGGJS18
Gilles Barthe, Xiong Fan, Joshua Gancher, Benjamin Grégoire, Charlie Jacomme, Elaine Shi:
Symbolic Proofs for Lattice-Based Cryptography. ACM Conference on Computer and Communications Security 2018: 538-555
[c60]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/cosade/GregoirePSS18
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cosade/GregoirePSS18
Benjamin Grégoire, Kostas Papagiannopoulos, Peter Schwabe, Ko Stoffelen:
Vectorizing Higher-Order Masking. COSADE 2018: 23-43
[c59]
- view
  - electronic edition via DOI
  - electronic edition @ ieeecomputersociety.org
- export record
  dblp key:
  - conf/csfw/Baritel-RuetDFG18
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/csfw/Baritel-RuetDFG18
Cecile Baritel-Ruet, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire:
Formal Security Proof of CMAC and Its Variants. CSF 2018: 91-104
[c58]
- view
  - electronic edition via DOI
  - electronic edition @ ieeecomputersociety.org
- export record
  dblp key:
  - conf/csfw/BartheGL18
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/csfw/BartheGL18
Gilles Barthe, Benjamin Grégoire, Vincent Laporte:
Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic "Constant-Time". CSF 2018: 328-343
[c57]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/esop/BartheEGGHS18
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/esop/BartheEGGHS18
Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
An Assertion-Based Program Logic for Probabilistic Programs. ESOP 2018: 117-144
[c56]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/eurocrypt/BartheBEFGRT18
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/eurocrypt/BartheBEFGRT18
Gilles Barthe, Sonia Belaïd, Thomas Espitau, Pierre-Alain Fouque, Benjamin Grégoire, Mélissa Rossi, Mehdi Tibouchi:
Masking the GLP Lattice-Based Signature Scheme at Any Order. EUROCRYPT (2) 2018: 354-384
[i24]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/abs-1803-05535
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/abs-1803-05535
Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
An Assertion-Based Program Logic for Probabilistic Programs. CoRR abs/1803.05535 (2018)
[i23]
- view
  - electronic edition @ iacr.org
- export record
  dblp key:
  - journals/iacr/GregoirePSS18
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/iacr/GregoirePSS18
Benjamin Grégoire, Kostas Papagiannopoulos, Peter Schwabe, Ko Stoffelen:
Vectorizing Higher-Order Masking. IACR Cryptology ePrint Archive 2018: 173 (2018)
[i22]
- view
  - electronic edition @ iacr.org
- export record
  dblp key:
  - journals/iacr/BartheBEFGRT18
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/iacr/BartheBEFGRT18
Gilles Barthe, Sonia Belaïd, Thomas Espitau, Pierre-Alain Fouque, Benjamin Grégoire, Mélissa Rossi, Mehdi Tibouchi:
Masking the GLP Lattice-Based Signature Scheme at Any Order. IACR Cryptology ePrint Archive 2018: 381 (2018)
[i21]
- view
  - electronic edition @ iacr.org
- export record
  dblp key:
  - journals/iacr/BartheBDFGSS18
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/iacr/BartheBDFGSS18
Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub:
Improved Parallel Mask Refreshing Algorithms: Generic Solutions with Parametrized Non-Interference & Automated Optimizations. IACR Cryptology ePrint Archive 2018: 505 (2018)
[i20]
- view
  - electronic edition @ iacr.org
- export record
  dblp key:
  - journals/iacr/BartheBFG18
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/iacr/BartheBFG18
Gilles Barthe, Sonia Belaïd, Pierre-Alain Fouque, Benjamin Grégoire:
maskVerif: a formal tool for analyzing software and hardware masked implementations. IACR Cryptology ePrint Archive 2018: 562 (2018)
[i19]
- view
  - electronic edition @ iacr.org
- export record
  dblp key:
  - journals/iacr/BartheFGGJS18
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/iacr/BartheFGGJS18
Gilles Barthe, Xiong Fan, Joshua Gancher, Benjamin Grégoire, Charlie Jacomme, Elaine Shi:
Symbolic Proofs for Lattice-Based Cryptography. IACR Cryptology ePrint Archive 2018: 765 (2018)
2017
[c55]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/ccs/AlmeidaBBBGLOPS17
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/ccs/AlmeidaBBBGLOPS17
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, Pierre-Yves Strub:
Jasmin: High-Assurance and High-Speed Cryptography. ACM Conference on Computer and Communications Security 2017: 1807-1823
[c54]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/ccs/AlmeidaBBDGLP17
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/ccs/AlmeidaBBDGLP17
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Vitor Pereira:
A Fast and Verified Software Stack for Secure Function Evaluation. ACM Conference on Computer and Communications Security 2017: 1989-2006
[c53]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/eurocrypt/BartheDFGSS17
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/eurocrypt/BartheDFGSS17
Gilles Barthe, François Dupressoir, Sebastian Faust, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub:
Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model. EUROCRYPT (1) 2017: 535-566
[c52]
- view
  - electronic edition @ easychair.org
- export record
  dblp key:
  - conf/lpar/BartheEGHS17
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/lpar/BartheEGHS17
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Proving uniformity and independence by self-composition and coupling. LPAR 2017: 385-403
[c51]
- view
  - electronic edition @ acm.org
- export record
  dblp key:
  - conf/popl/BartheGHS17
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/popl/BartheGHS17
Gilles Barthe, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Coupling proofs are probabilistic product programs. POPL 2017: 161-174
[i18]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/BartheEGHS17
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/BartheEGHS17
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Proving uniformity and independence by self-composition and coupling. CoRR abs/1701.06477 (2017)
[i17]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/abs-1708-02537
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/abs-1708-02537
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Proving Expected Sensitivity of Probabilistic Programs. CoRR abs/1708.02537 (2017)
[i16]
- view
  - electronic edition @ iacr.org
- export record
  dblp key:
  - journals/iacr/AlmeidaBBDGLP17
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/iacr/AlmeidaBBDGLP17
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Vitor Pereira:
A Fast and Verified Software Stack for Secure Function Evaluation. IACR Cryptology ePrint Archive 2017: 821 (2017)
[i15]
- view
  - electronic edition @ iacr.org
- export record
  dblp key:
  - journals/iacr/BartheDG17
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/iacr/BartheDG17
Gilles Barthe, François Dupressoir, Benjamin Grégoire:
A Note on 'Further Improving Efficiency of Higher-Order Masking Scheme by Decreasing Randomness Complexity'. IACR Cryptology ePrint Archive 2017: 1053 (2017)
[i14]
- view
  - electronic edition @ iacr.org
- export record
  dblp key:
  - journals/iacr/BartheGL17
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/iacr/BartheGL17
Gilles Barthe, Benjamin Grégoire, Vincent Laporte:
Provably secure compilation of side-channel countermeasures. IACR Cryptology ePrint Archive 2017: 1233 (2017)
2016
[c50]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/ccs/BartheFGGHS16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/ccs/BartheFGGHS16
Gilles Barthe, Noémie Fong, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Advanced Probabilistic Couplings for Differential Privacy. ACM Conference on Computer and Communications Security 2016: 55-67
[c49]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/ccs/BartheBDFGSZ16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/ccs/BartheBDFGSZ16
Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub, Rébecca Zucchini:
Strong Non-Interference and Type-Directed Higher-Order Masking. ACM Conference on Computer and Communications Security 2016: 116-129
[c48]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/icalp/BartheGGHS16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/icalp/BartheGGHS16
Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
A Program Logic for Union Bounds. ICALP 2016: 107:1-107:15
[c47]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/lics/BartheGGHS16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/lics/BartheGGHS16
Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Proving Differential Privacy via Probabilistic Couplings. LICS 2016: 749-758
[i13]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/BartheGGHS16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/BartheGGHS16
Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Proving Differential Privacy via Probabilistic Couplings. CoRR abs/1601.05047 (2016)
[i12]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/BartheGGHS16a
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/BartheGGHS16a
Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
A program logic for union bounds. CoRR abs/1602.05681 (2016)
[i11]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/BartheGGHS16b
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/BartheGGHS16b
Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Advanced Probabilistic Couplings for Differential Privacy. CoRR abs/1606.07143 (2016)
[i10]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/BartheGHS16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/BartheGHS16
Gilles Barthe, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Coupling proofs are probabilistic product programs. CoRR abs/1607.03455 (2016)
[i9]
- view
  - electronic edition @ iacr.org
- export record
  dblp key:
  - journals/iacr/BartheDFGSS16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/iacr/BartheDFGSS16
Gilles Barthe, François Dupressoir, Sebastian Faust, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub:
Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model. IACR Cryptology ePrint Archive 2016: 912 (2016)
2015
[c46]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/ccs/BartheGS15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/ccs/BartheGS15
Gilles Barthe, Benjamin Grégoire, Benedikt Schmidt:
Automated Proofs of Pairing-Based Cryptography. ACM Conference on Computer and Communications Security 2015: 1156-1168
[c45]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/eurocrypt/BartheBDFGS15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/eurocrypt/BartheBDFGS15
Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub:
Verified Proofs of Higher-Order Masking. EUROCRYPT (1) 2015: 457-485
[c44]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/lpar/BartheEGHSS15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/lpar/BartheEGHSS15
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Léo Stefanesco, Pierre-Yves Strub:
Relational Reasoning via Probabilistic Coupling. LPAR 2015: 387-401
[i8]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/BartheEGHSS15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/BartheEGHSS15
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Léo Stefanesco, Pierre-Yves Strub:
Relational reasoning via probabilistic coupling. CoRR abs/1509.03476 (2015)
[i7]
- view
  - electronic edition @ iacr.org
- export record
  dblp key:
  - journals/iacr/BartheBDFGS15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/iacr/BartheBDFGS15
Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub:
Verified Proofs of Higher-Order Masking. IACR Cryptology ePrint Archive 2015: 60 (2015)
[i6]
- view
  - electronic edition @ iacr.org
- export record
  dblp key:
  - journals/iacr/BartheBDFG15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/iacr/BartheBDFG15
Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire:
Compositional Verification of Higher-Order Masking: Application to a Verifying Masking Compiler. IACR Cryptology ePrint Archive 2015: 506 (2015)
2014
[c43]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/ccs/BartheDFGZ14
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/ccs/BartheDFGZ14
Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Jean-Christophe Zapalowicz:
Synthesis of Fault Attacks on Cryptographic Implementations. ACM Conference on Computer and Communications Security 2014: 1016-1027
[c42]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/ches/BartheDFGTZ14
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/ches/BartheDFGTZ14
Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Mehdi Tibouchi, Jean-Christophe Zapalowicz:
Making RSA-PSS Provably Secure against Non-random Faults. CHES 2014: 206-222
[c41]
- view
  - electronic edition via DOI
  - electronic edition @ ieeecomputersociety.org
- export record
  dblp key:
  - conf/csfw/AkinyeleBGSS14
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/csfw/AkinyeleBGSS14
Joseph A. Akinyele, Gilles Barthe, Benjamin Grégoire, Benedikt Schmidt, Pierre-Yves Strub:
Certified Synthesis of Efficient Batch Verifiers. CSF 2014: 153-165
[c40]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/popl/BartheFGSSB14
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/popl/BartheFGSSB14
Gilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Nikhil Swamy, Santiago Zanella Béguelin:
Probabilistic relational verification for cryptographic implementations. POPL 2014: 193-206
[i5]
- view
  - electronic edition @ iacr.org
- export record
  dblp key:
  - journals/iacr/BartheDFGTZ14
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/iacr/BartheDFGTZ14
Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Mehdi Tibouchi, Jean-Christophe Zapalowicz:
Making RSA-PSS Provably Secure Against Non-Random Faults. IACR Cryptology ePrint Archive 2014: 252 (2014)
[i4]
- view
  - electronic edition @ iacr.org
- export record
  dblp key:
  - journals/iacr/BartheDFGZ14
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/iacr/BartheDFGZ14
Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Jean-Christophe Zapalowicz:
Synthesis of Fault Attacks on Cryptographic Implementations. IACR Cryptology ePrint Archive 2014: 436 (2014)
[i3]
- view
  - electronic edition @ iacr.org
- export record
  dblp key:
  - journals/iacr/AlmeidaBBDDGS14
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/iacr/AlmeidaBBDDGS14
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Guillaume Davy, François Dupressoir, Benjamin Grégoire, Pierre-Yves Strub:
Verified Implementations for Secure and Verifiable Computation. IACR Cryptology ePrint Archive 2014: 456 (2014)
2013
[j3]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - journals/jcs/BartheGHOB13
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/jcs/BartheGHOB13
Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Federico Olmedo, Santiago Zanella Béguelin:
Verified indifferentiable hashing into elliptic curves. Journal of Computer Security 21(6): 881-917 (2013)
[c39]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/ccs/BartheCGKLSB13
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/ccs/BartheCGKLSB13
Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Benedikt Schmidt, Santiago Zanella Béguelin:
Fully automated analysis of padding-based encryption in the computational model. ACM Conference on Computer and Communications Security 2013: 1247-1260
[c38]
- view
  - electronic edition via DOI
  - electronic edition @ ieeecomputersociety.org
- export record
  dblp key:
  - conf/csfw/BartheDGKB13
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/csfw/BartheDGKB13
Gilles Barthe, George Danezis, Benjamin Grégoire, César Kunz, Santiago Zanella Béguelin:
Verified Computational Differential Privacy with Applications to Smart Metering. CSF 2013: 287-301
[c37]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/fosad/BartheDGKSS13
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/fosad/BartheDGKSS13
Gilles Barthe, François Dupressoir, Benjamin Grégoire, César Kunz, Benedikt Schmidt, Pierre-Yves Strub:
EasyCrypt: A Tutorial. FOSAD 2013: 146-166
2012
[c36]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/cpp/BartheGKLB12
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/BartheGKLB12
Gilles Barthe, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Santiago Zanella Béguelin:
Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs. CPP 2012: 7-8
[c35]
- view
  - electronic edition via DOI
  - electronic edition @ ieeecomputersociety.org
- export record
  dblp key:
  - conf/csfw/BackesBBGKSB12
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/csfw/BackesBBGKSB12
Michael Backes, Gilles Barthe, Matthias Berg, Benjamin Grégoire, César Kunz, Malte Skoruppa, Santiago Zanella Béguelin:
Verified Security of Merkle-Damgård. CSF 2012: 354-368
[c34]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/itp/BartheCGKB12
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/itp/BartheCGKB12
Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Santiago Zanella Béguelin:
Computer-Aided Cryptographic Proofs. ITP 2012: 11-27
[c33]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/mpc/BartheGB12
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/mpc/BartheGB12
Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin:
Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs. MPC 2012: 1-6
[c32]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/post/BartheGHOB12
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/post/BartheGHOB12
Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Federico Olmedo, Santiago Zanella Béguelin:
Verified Indifferentiable Hashing into Elliptic Curves. POST 2012: 209-228
[c31]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/sas/BartheGB12
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/sas/BartheGB12
Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin:
Computer-Aided Cryptographic Proofs. SAS 2012: 1-2
[i2]
- view
  - electronic edition @ ercim.eu
- export record
  dblp key:
  - journals/ercim/Gregoire12
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/ercim/Gregoire12
Benjamin Grégoire:
Recent Advances in the Formal Verification of Cryptographic Systems: Turing's Legacy. ERCIM News 2012(91) (2012)
[i1]
- view
  - electronic edition @ iacr.org
- export record
  dblp key:
  - journals/iacr/BartheCGKLB12
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/iacr/BartheCGKLB12
Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Santiago Zanella Béguelin:
Automated Analysis and Synthesis of Padding-Based Encryption Schemes. IACR Cryptology ePrint Archive 2012: 695 (2012)
2011
[j2]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - journals/fmsd/BlechG11
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/fmsd/BlechG11
Jan Olaf Blech, Benjamin Grégoire:
Certifying compilers using higher-order theorem provers as certificate checkers. Formal Methods in System Design 38(1): 33-61 (2011)
[c30]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/cpp/ArmandFGKTW11
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/ArmandFGKTW11
Michaël Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry, Benjamin Werner:
A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses. CPP 2011: 135-150
[c29]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/cpp/BoespflugDG11
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/BoespflugDG11
Mathieu Boespflug, Maxime Dénès, Benjamin Grégoire:
Full Reduction at Full Throttle. CPP 2011: 362-377
[c28]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/crypto/BartheGHB11
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/crypto/BartheGHB11
Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Santiago Zanella Béguelin:
Computer-Aided Security Proofs for the Working Cryptographer. CRYPTO 2011: 71-90
[c27]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/ctrsa/BartheGLB11
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/ctrsa/BartheGLB11
Gilles Barthe, Benjamin Grégoire, Yassine Lakhnech, Santiago Zanella Béguelin:
Beyond Provable Security Verifiable IND-CCA Security of OAEP. CT-RSA 2011: 180-196
2010
[c26]
- view
  - electronic edition via DOI
  - electronic edition @ ieeecomputersociety.org
- export record
  dblp key:
  - conf/csfw/BartheHBGH10
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/csfw/BartheHBGH10
Gilles Barthe, Daniel Hedin, Santiago Zanella Béguelin, Benjamin Grégoire, Sylvain Heraud:
A Machine-Checked Formalization of Sigma-Protocols. CSF 2010: 246-260
[c25]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/itp/ArmandGST10
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/itp/ArmandGST10
Michaël Armand, Benjamin Grégoire, Arnaud Spiwack, Laurent Théry:
Extending Coq with Imperative Features and Its Application to SAT Verification. ITP 2010: 83-98
[c24]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/itp/BartheGB10
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/itp/BartheGB10
Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin:
Programming Language Techniques for Cryptographic Proofs. ITP 2010: 115-130
[c23]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/lpar/GregoireS10
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/lpar/GregoireS10
Benjamin Grégoire, Jorge Luis Sacchini:
On Strong Normalization of the Calculus of Constructions with Type-Based Termination. LPAR (Yogyakarta) 2010: 333-347

2000 – 2009

see FAQ

What is the meaning of the colors in the publication lists?

2009
[j1]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - journals/toplas/BartheGKR09
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/toplas/BartheGKR09
Gilles Barthe, Benjamin Grégoire, César Kunz, Tamara Rezk:
Certificate translation for optimizing compilers. ACM Trans. Program. Lang. Syst. 31(5): 18:1-18:45 (2009)
[c22]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/icfem/BartheGHKP09
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/icfem/BartheGHKP09
Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, César Kunz, Anne Pacalet:
Implementing a Direct Method for Certificate Translation. ICFEM 2009: 541-560
[c21]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/popl/BartheGB09
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/popl/BartheGB09
Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin:
Formal certification of code-based cryptographic proofs. POPL 2009: 90-101
[c20]
- view
  - electronic edition via DOI
  - electronic edition @ ieeecomputersociety.org
- export record
  dblp key:
  - conf/sp/BeguelinBGO09
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/sp/BeguelinBGO09
Santiago Zanella Béguelin, Gilles Barthe, Benjamin Grégoire, Federico Olmedo:
Formally Certifying the Security of Digital Signature Schemes. IEEE Symposium on Security and Privacy 2009: 237-250
2008
[c19]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/adg/GregoirePT08
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/adg/GregoirePT08
Benjamin Grégoire, Loïc Pottier, Laurent Théry:
Proof Certificates for Algebra and Their Application to Automatic Geometry Theorem Proving. Automated Deduction in Geometry 2008: 42-59
[c18]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/cade/BartheGP08
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cade/BartheGP08
Gilles Barthe, Benjamin Grégoire, Mariela Pavlova:
Preservation of Proof Obligations from Java to the Java Virtual Machine. IJCAR 2008: 83-99
[c17]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/csl/BartheGR08
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/csl/BartheGR08
Gilles Barthe, Benjamin Grégoire, Colin Riba:
Type-Based Termination with Sized Products. CSL 2008: 493-507
[c16]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/ifip1-7/BartheGHB08
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/ifip1-7/BartheGHB08
Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Santiago Zanella Béguelin:
Formal Certification of ElGamal Encryption. Formal Aspects in Security and Trust 2008: 1-19
[c15]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/lernet/BartheGR08
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/lernet/BartheGR08
Gilles Barthe, Benjamin Grégoire, Colin Riba:
A Tutorial on Type-Based Termination. LerNet ALFA Summer School 2008: 100-152
[c14]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/types/BarrasCGHS08
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/types/BarrasCGHS08
Bruno Barras, Pierre Corbineau, Benjamin Grégoire, Hugo Herbelin, Jorge Luis Sacchini:
A New Elimination Rule for the Calculus of Inductive Constructions. TYPES 2008: 32-48
2007
[c13]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/fmco/BartheCGJP07
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/fmco/BartheCGJP07
Gilles Barthe, Pierre Crégut, Benjamin Grégoire, Thomas P. Jensen, David Pichardie:
The MOBIUS Proof Carrying Code Infrastructure. FMCO 2007: 1-24
[c12]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tgc/GregoireS07
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tgc/GregoireS07
Benjamin Grégoire, Jorge Luis Sacchini:
Combining a Verification Condition Generator for a Bytecode Language with Static Analyses. TGC 2007: 23-40
2006
[c11]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/cade/GregoireT06
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cade/GregoireT06
Benjamin Grégoire, Laurent Théry:
A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers. IJCAR 2006: 423-437
[c10]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/flops/GregoireTW06
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/flops/GregoireTW06
Benjamin Grégoire, Laurent Théry, Benjamin Werner:
A Computational Approach to Pocklington Certificates in Type Theory. FLOPS 2006: 97-113
[c9]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/fmco/BartheBCGHLPR06
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/fmco/BartheBCGHLPR06
Gilles Barthe, Lilian Burdy, Julien Charles, Benjamin Grégoire, Marieke Huisman, Jean-Louis Lanet, Mariela Pavlova, Antoine Requet:
JACK - A Tool for Validation of Security and Behaviour of Java Applications. FMCO 2006: 152-174
[c8]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/lpar/BartheGP06
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/lpar/BartheGP06
Gilles Barthe, Benjamin Grégoire, Fernando Pastawski:
CIC[^( )]: Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions. LPAR 2006: 257-271
[c7]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/sas/BartheGKR06
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/sas/BartheGKR06
Gilles Barthe, Benjamin Grégoire, César Kunz, Tamara Rezk:
Certificate Translation for Optimizing Compilers. SAS 2006: 301-317
[c6]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tgc/BartheBCGHMPPSV06
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tgc/BartheBCGHMPPSV06
Gilles Barthe, Lennart Beringer, Pierre Crégut, Benjamin Grégoire, Martin Hofmann, Peter Müller, Erik Poll, Germán Puebla, Ian Stark, Eric Vétillard:
MOBIUS: Mobility, Ubiquity, Security. TGC 2006: 10-29
[e1]
- view
  - table of contents in dblp
  - electronic edition via DOI
- export record
  dblp key:
  - conf/cassis/2005
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cassis/2005
Gilles Barthe, Benjamin Grégoire, Marieke Huisman, Jean-Louis Lanet:
Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, Second International Workshop, CASSIS 2005, Nice, France, March 8-11, 2005, Revised Selected Papers. Lecture Notes in Computer Science 3956, Springer 2006, ISBN 3-540-33689-3 [contents]
2005
[c5]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/csl/BarrasG05
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/csl/BarrasG05
Bruno Barras, Benjamin Grégoire:
On the Role of Type Decorations in the Calculus of Inductive Constructions. CSL 2005: 151-166
[c4]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tlca/BartheGP05
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tlca/BartheGP05
Gilles Barthe, Benjamin Grégoire, Fernando Pastawski:
Practical Inference for Type-Based Termination in a Polymorphic Setting. TLCA 2005: 71-85
[c3]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tphol/GregoireM05
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tphol/GregoireM05
Benjamin Grégoire, Assia Mahboubi:
Proving Equalities in a Commutative Ring Done Right in Coq. TPHOLs 2005: 98-113
2004
[c2]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/types/BertotGL04
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/types/BertotGL04
Yves Bertot, Benjamin Grégoire, Xavier Leroy:
A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis. TYPES 2004: 66-81
2002
[c1]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/icfp/GregoireL02
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/icfp/GregoireL02
Benjamin Grégoire, Xavier Leroy:
A compiled implementation of strong reduction. ICFP 2002: 235-246

Coauthor Index

see FAQ

maintained by

at