Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDBibTeX records: Benjamin Grégoire
@article{DBLP:journals/joc/BartheBEFGRT24,
author = {Gilles Barthe and
Sonia Bela{\"{\i}}d and
Thomas Espitau and
Pierre{-}Alain Fouque and
Benjamin Gr{\'{e}}goire and
M{\'{e}}lissa Rossi and
Mehdi Tibouchi},
title = {Masking the {GLP} Lattice-Based Signature Scheme at Any Order},
journal = {J. Cryptol.},
volume = {37},
number = {1},
pages = {5},
year = {2024},
url = {https://doi.org/10.1007/s00145-023-09485-z},
doi = {10.1007/S00145-023-09485-Z},
timestamp = {Mon, 15 Jan 2024 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/joc/BartheBEFGRT24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tches/OlmosBGGLLOS24,
author = {Santiago Arranz Olmos and
Gilles Barthe and
Ruben Gonzalez and
Benjamin Gr{\'{e}}goire and
Vincent Laporte and
Jean{-}Christophe L{\'{e}}chenet and
Tiago Oliveira and
Peter Schwabe},
title = {High-assurance zeroization},
journal = {{IACR} Trans. Cryptogr. Hardw. Embed. Syst.},
volume = {2024},
number = {1},
pages = {375--397},
year = {2024},
url = {https://doi.org/10.46586/tches.v2024.i1.375-397},
doi = {10.46586/TCHES.V2024.I1.375-397},
timestamp = {Tue, 02 Jan 2024 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/tches/OlmosBGGLLOS24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tches/AlmeidaBBGLL00Q23,
author = {Jos{\'{e}} Bacelar Almeida and
Manuel Barbosa and
Gilles Barthe and
Benjamin Gr{\'{e}}goire and
Vincent Laporte and
Jean{-}Christophe L{\'{e}}chenet and
Tiago Oliveira and
Hugo Pacheco and
Miguel Quaresma and
Peter Schwabe and
Antoine S{\'{e}}r{\'{e}} and
Pierre{-}Yves Strub},
title = {Formally verifying Kyber Episode {IV:} Implementation correctness},
journal = {{IACR} Trans. Cryptogr. Hardw. Embed. Syst.},
volume = {2023},
number = {3},
pages = {164--193},
year = {2023},
url = {https://doi.org/10.46586/tches.v2023.i3.164-193},
doi = {10.46586/TCHES.V2023.I3.164-193},
timestamp = {Mon, 05 Feb 2024 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/tches/AlmeidaBBGLL00Q23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tissec/BarbosaBGKS23,
author = {Manuel Barbosa and
Gilles Barthe and
Benjamin Gr{\'{e}}goire and
Adrien Koutsos and
Pierre{-}Yves Strub},
title = {Mechanized Proofs of Adversarial Complexity and Application to Universal
Composability},
journal = {{ACM} Trans. Priv. Secur.},
volume = {26},
number = {3},
pages = {41:1--41:34},
year = {2023},
url = {https://doi.org/10.1145/3589962},
doi = {10.1145/3589962},
timestamp = {Thu, 09 Nov 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/tissec/BarbosaBGKS23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/GregoireLT23,
author = {Benjamin Gr{\'{e}}goire and
Jean{-}Christophe L{\'{e}}chenet and
Enrico Tassi},
editor = {Robbert Krebbers and
Dmitriy Traytel and
Brigitte Pientka and
Steve Zdancewic},
title = {Practical and Sound Equality Tests, Automatically: Deriving eqType
Instances for Jasmin's Data Types with Coq-Elpi},
booktitle = {Proceedings of the 12th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2023, Boston, MA, USA, January
16-17, 2023},
pages = {167--181},
publisher = {{ACM}},
year = {2023},
url = {https://doi.org/10.1145/3573105.3575683},
doi = {10.1145/3573105.3575683},
timestamp = {Tue, 21 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/GregoireLT23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/crypto/BarbosaBDDFGHHLW22,
author = {Manuel Barbosa and
Gilles Barthe and
Christian Doczkal and
Jelle Don and
Serge Fehr and
Benjamin Gr{\'{e}}goire and
Yu{-}Hsuan Huang and
Andreas H{\"{u}}lsing and
Yi Lee and
Xiaodi Wu},
editor = {Helena Handschuh and
Anna Lysyanskaya},
title = {Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts
and Dilithium},
booktitle = {Advances in Cryptology - {CRYPTO} 2023 - 43rd Annual International
Cryptology Conference, {CRYPTO} 2023, Santa Barbara, CA, USA, August
20-24, 2023, Proceedings, Part {V}},
series = {Lecture Notes in Computer Science},
volume = {14085},
pages = {358--389},
publisher = {Springer},
year = {2023},
url = {https://doi.org/10.1007/978-3-031-38554-4\_12},
doi = {10.1007/978-3-031-38554-4\_12},
timestamp = {Sun, 17 Dec 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/crypto/BarbosaBDDFGHHLW22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/crypto/BarbosaDGHMS22,
author = {Manuel Barbosa and
Fran{\c{c}}ois Dupressoir and
Benjamin Gr{\'{e}}goire and
Andreas H{\"{u}}lsing and
Matthias Meijers and
Pierre{-}Yves Strub},
editor = {Helena Handschuh and
Anna Lysyanskaya},
title = {Machine-Checked Security for rmXMSS as in {RFC} 8391 and {\textdollar}{\textbackslash}mathrm
\{SPHINCS{\^{}}\{+\}\} {\textdollar}},
booktitle = {Advances in Cryptology - {CRYPTO} 2023 - 43rd Annual International
Cryptology Conference, {CRYPTO} 2023, Santa Barbara, CA, USA, August
20-24, 2023, Proceedings, Part {V}},
series = {Lecture Notes in Computer Science},
volume = {14085},
pages = {421--454},
publisher = {Springer},
year = {2023},
url = {https://doi.org/10.1007/978-3-031-38554-4\_14},
doi = {10.1007/978-3-031-38554-4\_14},
timestamp = {Tue, 26 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/crypto/BarbosaDGHMS22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sp/ShivakumarBGLOPST23,
author = {Basavesh Ammanaghatta Shivakumar and
Gilles Barthe and
Benjamin Gr{\'{e}}goire and
Vincent Laporte and
Tiago Oliveira and
Swarn Priya and
Peter Schwabe and
Lucas Tabary{-}Maujean},
title = {Typing High-Speed Cryptography against Spectre v1},
booktitle = {44th {IEEE} Symposium on Security and Privacy, {SP} 2023, San Francisco,
CA, USA, May 21-25, 2023},
pages = {1094--1111},
publisher = {{IEEE}},
year = {2023},
url = {https://doi.org/10.1109/SP46215.2023.10179418},
doi = {10.1109/SP46215.2023.10179418},
timestamp = {Thu, 27 Jul 2023 08:17:10 +0200},
biburl = {https://dblp.org/rec/conf/sp/ShivakumarBGLOPST23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iacr/AlmeidaBBGLLOPQSSS23,
author = {Jos{\'{e}} Bacelar Almeida and
Manuel Barbosa and
Gilles Barthe and
Benjamin Gr{\'{e}}goire and
Vincent Laporte and
Jean{-}Christophe L{\'{e}}chenet and
Tiago Oliveira and
Hugo Pacheco and
Miguel Quaresma and
Peter Schwabe and
Antoine S{\'{e}}r{\'{e}} and
Pierre{-}Yves Strub},
title = {Formally verifying Kyber Part {I:} Implementation Correctness},
journal = {{IACR} Cryptol. ePrint Arch.},
pages = {215},
year = {2023},
url = {https://eprint.iacr.org/2023/215},
timestamp = {Tue, 28 Feb 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/iacr/AlmeidaBBGLLOPQSSS23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iacr/BarbosaBDDFGHHLW23,
author = {Manuel Barbosa and
Gilles Barthe and
Christian Doczkal and
Jelle Don and
Serge Fehr and
Benjamin Gr{\'{e}}goire and
Yu{-}Hsuan Huang and
Andreas H{\"{u}}lsing and
Yi Lee and
Xiaodi Wu},
title = {Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts
and Dilithium},
journal = {{IACR} Cryptol. ePrint Arch.},
pages = {246},
year = {2023},
url = {https://eprint.iacr.org/2023/246},
timestamp = {Sun, 17 Dec 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/iacr/BarbosaBDDFGHHLW23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iacr/BarbosaDGHMS23,
author = {Manuel Barbosa and
Fran{\c{c}}ois Dupressoir and
Benjamin Gr{\'{e}}goire and
Andreas H{\"{u}}lsing and
Matthias Meijers and
Pierre{-}Yves Strub},
title = {Machine-Checked Security for {\textdollar}{\textbackslash}mathrm\{XMSS\}{\textdollar}
as in {RFC} 8391 and {\textdollar}{\textbackslash}mathrm\{SPHINCS\}{\^{}}\{+\}{\textdollar}},
journal = {{IACR} Cryptol. ePrint Arch.},
pages = {408},
year = {2023},
url = {https://eprint.iacr.org/2023/408},
timestamp = {Fri, 31 Mar 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/iacr/BarbosaDGHMS23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iacr/OlmosBGGLLOS23,
author = {Santiago Arranz Olmos and
Gilles Barthe and
Ruben Gonzalez and
Benjamin Gr{\'{e}}goire and
Vincent Laporte and
Jean{-}Christophe L{\'{e}}chenet and
Tiago Oliveira and
Peter Schwabe},
title = {High-assurance zeroization},
journal = {{IACR} Cryptol. ePrint Arch.},
pages = {1713},
year = {2023},
url = {https://eprint.iacr.org/2023/1713},
timestamp = {Thu, 09 Nov 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/iacr/OlmosBGGLLOS23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ccs/ShivakumarBGLP22,
author = {Basavesh Ammanaghatta Shivakumar and
Gilles Barthe and
Benjamin Gr{\'{e}}goire and
Vincent Laporte and
Swarn Priya},
editor = {Heng Yin and
Angelos Stavrou and
Cas Cremers and
Elaine Shi},
title = {Enforcing Fine-grained Constant-time Policies},
booktitle = {Proceedings of the 2022 {ACM} {SIGSAC} Conference on Computer and
Communications Security, {CCS} 2022, Los Angeles, CA, USA, November
7-11, 2022},
pages = {83--96},
publisher = {{ACM}},
year = {2022},
url = {https://doi.org/10.1145/3548606.3560689},
doi = {10.1145/3548606.3560689},
timestamp = {Sat, 17 Dec 2022 01:15:29 +0100},
biburl = {https://dblp.org/rec/conf/ccs/ShivakumarBGLP22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iacr/ShivakumarBGLP22,
author = {Basavesh Ammanaghatta Shivakumar and
Gilles Barthe and
Benjamin Gr{\'{e}}goire and
Vincent Laporte and
Swarn Priya},
title = {Enforcing fine-grained constant-time policies},
journal = {{IACR} Cryptol. ePrint Arch.},
pages = {630},
year = {2022},
url = {https://eprint.iacr.org/2022/630},
timestamp = {Mon, 20 Jun 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/iacr/ShivakumarBGLP22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iacr/ShivakumarBGLOP22,
author = {Basavesh Ammanaghatta Shivakumar and
Gilles Barthe and
Benjamin Gr{\'{e}}goire and
Vincent Laporte and
Tiago Oliveira and
Swarn Priya and
Peter Schwabe and
Lucas Tabary{-}Maujean},
title = {Typing High-Speed Cryptography against Spectre v1},
journal = {{IACR} Cryptol. ePrint Arch.},
pages = {1270},
year = {2022},
url = {https://eprint.iacr.org/2022/1270},
timestamp = {Sat, 22 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/iacr/ShivakumarBGLOP22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tc/CassiersGLS21,
author = {Ga{\"{e}}tan Cassiers and
Benjamin Gr{\'{e}}goire and
Itamar Levi and
Fran{\c{c}}ois{-}Xavier Standaert},
title = {Hardware Private Circuits: From Trivial Composition to Full Verification},
journal = {{IEEE} Trans. Computers},
volume = {70},
number = {10},
pages = {1677--1690},
year = {2021},
url = {https://doi.org/10.1109/TC.2020.3022979},
doi = {10.1109/TC.2020.3022979},
timestamp = {Wed, 23 Feb 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/tc/CassiersGLS21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tches/BartheGGOPP21,
author = {Gilles Barthe and
Marc Gourjon and
Benjamin Gr{\'{e}}goire and
Maximilian Orlt and
Clara Paglialonga and
Lars Porth},
title = {Masking in Fine-Grained Leakage Models: Construction, Implementation
and Verification},
journal = {{IACR} Trans. Cryptogr. Hardw. Embed. Syst.},
volume = {2021},
number = {2},
pages = {189--228},
year = {2021},
url = {https://doi.org/10.46586/tches.v2021.i2.189-228},
doi = {10.46586/TCHES.V2021.I2.189-228},
timestamp = {Mon, 28 Aug 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/tches/BartheGGOPP21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ccs/BartheGLP21,
author = {Gilles Barthe and
Benjamin Gr{\'{e}}goire and
Vincent Laporte and
Swarn Priya},
editor = {Yongdae Kim and
Jong Kim and
Giovanni Vigna and
Elaine Shi},
title = {Structured Leakage and Applications to Cryptographic Constant-Time
and Cost},
booktitle = {{CCS} '21: 2021 {ACM} {SIGSAC} Conference on Computer and Communications
Security, Virtual Event, Republic of Korea, November 15 - 19, 2021},
pages = {462--476},
publisher = {{ACM}},
year = {2021},
url = {https://doi.org/10.1145/3460120.3484761},
doi = {10.1145/3460120.3484761},
timestamp = {Tue, 16 Nov 2021 12:59:46 +0100},
biburl = {https://dblp.org/rec/conf/ccs/BartheGLP21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ccs/BarbosaBGKS21,
author = {Manuel Barbosa and
Gilles Barthe and
Benjamin Gr{\'{e}}goire and
Adrien Koutsos and
Pierre{-}Yves Strub},
editor = {Yongdae Kim and
Jong Kim and
Giovanni Vigna and
Elaine Shi},
title = {Mechanized Proofs of Adversarial Complexity and Application to Universal
Composability},
booktitle = {{CCS} '21: 2021 {ACM} {SIGSAC} Conference on Computer and Communications
Security, Virtual Event, Republic of Korea, November 15 - 19, 2021},
pages = {2541--2563},
publisher = {{ACM}},
year = {2021},
url = {https://doi.org/10.1145/3460120.3484548},
doi = {10.1145/3460120.3484548},
timestamp = {Thu, 23 Jun 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/ccs/BarbosaBGKS21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ccs/BarbosaBFGHKSWZ21,
author = {Manuel Barbosa and
Gilles Barthe and
Xiong Fan and
Benjamin Gr{\'{e}}goire and
Shih{-}Han Hung and
Jonathan Katz and
Pierre{-}Yves Strub and
Xiaodi Wu and
Li Zhou},
editor = {Yongdae Kim and
Jong Kim and
Giovanni Vigna and
Elaine Shi},
title = {EasyPQC: Verifying Post-Quantum Cryptography},
booktitle = {{CCS} '21: 2021 {ACM} {SIGSAC} Conference on Computer and Communications
Security, Virtual Event, Republic of Korea, November 15 - 19, 2021},
pages = {2564--2586},
publisher = {{ACM}},
year = {2021},
url = {https://doi.org/10.1145/3460120.3484567},
doi = {10.1145/3460120.3484567},
timestamp = {Sun, 17 Dec 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/ccs/BarbosaBFGHKSWZ21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sp/BartheCGKLOPRS21,
author = {Gilles Barthe and
Sunjay Cauligi and
Benjamin Gr{\'{e}}goire and
Adrien Koutsos and
Kevin Liao and
Tiago Oliveira and
Swarn Priya and
Tamara Rezk and
Peter Schwabe},
title = {High-Assurance Cryptography in the Spectre Era},
booktitle = {42nd {IEEE} Symposium on Security and Privacy, {SP} 2021, San Francisco,
CA, USA, 24-27 May 2021},
pages = {1884--1901},
publisher = {{IEEE}},
year = {2021},
url = {https://doi.org/10.1109/SP40001.2021.00046},
doi = {10.1109/SP40001.2021.00046},
timestamp = {Thu, 21 Sep 2023 15:57:26 +0200},
biburl = {https://dblp.org/rec/conf/sp/BartheCGKLOPRS21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iacr/BarbosaBGKS21,
author = {Manuel Barbosa and
Gilles Barthe and
Benjamin Gr{\'{e}}goire and
Adrien Koutsos and
Pierre{-}Yves Strub},
title = {Mechanized Proofs of Adversarial Complexity and Application to Universal
Composability},
journal = {{IACR} Cryptol. ePrint Arch.},
pages = {156},
year = {2021},
url = {https://eprint.iacr.org/2021/156},
timestamp = {Tue, 02 Mar 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/iacr/BarbosaBGKS21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iacr/BartheGLP21,
author = {Gilles Barthe and
Benjamin Gr{\'{e}}goire and
Vincent Laporte and
Swarn Priya},
title = {Structured Leakage and Applications to Cryptographic Constant-Time
and Cost},
journal = {{IACR} Cryptol. ePrint Arch.},
pages = {650},
year = {2021},
url = {https://eprint.iacr.org/2021/650},
timestamp = {Mon, 07 Jun 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/iacr/BartheGLP21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iacr/BarbosaBFGHKSWZ21,
author = {Manuel Barbosa and
Gilles Barthe and
Xiong Fan and
Benjamin Gr{\'{e}}goire and
Shih{-}Han Hung and
Jonathan Katz and
Pierre{-}Yves Strub and
Xiaodi Wu and
Li Zhou},
title = {EasyPQC: Verifying Post-Quantum Cryptography},
journal = {{IACR} Cryptol. ePrint Arch.},
pages = {1253},
year = {2021},
url = {https://eprint.iacr.org/2021/1253},
timestamp = {Sun, 17 Dec 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/iacr/BarbosaBFGHKSWZ21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jce/BartheBDFGSS20,
author = {Gilles Barthe and
Sonia Bela{\"{\i}}d and
Fran{\c{c}}ois Dupressoir and
Pierre{-}Alain Fouque and
Benjamin Gr{\'{e}}goire and
Fran{\c{c}}ois{-}Xavier Standaert and
Pierre{-}Yves Strub},
title = {Improved parallel mask refreshing algorithms: generic solutions with
parametrized non-interference and automated optimizations},
journal = {J. Cryptogr. Eng.},
volume = {10},
number = {1},
pages = {17--26},
year = {2020},
url = {https://doi.org/10.1007/s13389-018-00202-2},
doi = {10.1007/S13389-018-00202-2},
timestamp = {Thu, 14 Oct 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jce/BartheBDFGSS20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/pacmpl/BartheBGHLPT20,
author = {Gilles Barthe and
Sandrine Blazy and
Benjamin Gr{\'{e}}goire and
R{\'{e}}mi Hutin and
Vincent Laporte and
David Pichardie and
Alix Trieu},
title = {Formal verification of a constant-time preserving {C} compiler},
journal = {Proc. {ACM} Program. Lang.},
volume = {4},
number = {{POPL}},
pages = {7:1--7:30},
year = {2020},
url = {https://doi.org/10.1145/3371075},
doi = {10.1145/3371075},
timestamp = {Mon, 28 Aug 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/pacmpl/BartheBGHLPT20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/icete/LazGR20,
author = {Mohamad El Laz and
Benjamin Gr{\'{e}}goire and
Tamara Rezk},
editor = {Pierangela Samarati and
Sabrina De Capitani di Vimercati and
Mohammad S. Obaidat and
Jalel Ben{-}Othman},
title = {Security Analysis of ElGamal Implementations},
booktitle = {Proceedings of the 17th International Joint Conference on e-Business
and Telecommunications, {ICETE} 2020 - Volume 2: SECRYPT, Lieusaint,
Paris, France, July 8-10, 2020},
pages = {310--321},
publisher = {ScitePress},
year = {2020},
url = {https://doi.org/10.5220/0009817103100321},
doi = {10.5220/0009817103100321},
timestamp = {Wed, 29 Jul 2020 16:57:35 +0200},
biburl = {https://dblp.org/rec/conf/icete/LazGR20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sp/AlmeidaBBGKL0S20,
author = {Jos{\'{e}} Bacelar Almeida and
Manuel Barbosa and
Gilles Barthe and
Benjamin Gr{\'{e}}goire and
Adrien Koutsos and
Vincent Laporte and
Tiago Oliveira and
Pierre{-}Yves Strub},
title = {The Last Mile: High-Assurance and High-Speed Cryptographic Implementations},
booktitle = {2020 {IEEE} Symposium on Security and Privacy, {SP} 2020, San Francisco,
CA, USA, May 18-21, 2020},
pages = {965--982},
publisher = {{IEEE}},
year = {2020},
url = {https://doi.org/10.1109/SP40000.2020.00028},
doi = {10.1109/SP40000.2020.00028},
timestamp = {Thu, 21 Sep 2023 15:57:24 +0200},
biburl = {https://dblp.org/rec/conf/sp/AlmeidaBBGKL0S20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iacr/CassiersGLS20,
author = {Ga{\"{e}}tan Cassiers and
Benjamin Gr{\'{e}}goire and
Itamar Levi and
Fran{\c{c}}ois{-}Xavier Standaert},
title = {Hardware Private Circuits: From Trivial Composition to Full Verification},
journal = {{IACR} Cryptol. ePrint Arch.},
pages = {185},
year = {2020},
url = {https://eprint.iacr.org/2020/185},
timestamp = {Mon, 11 May 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/iacr/CassiersGLS20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iacr/BartheGGOPP20,
author = {Gilles Barthe and
Marc Gourjon and
Benjamin Gr{\'{e}}goire and
Maximilian Orlt and
Clara Paglialonga and
Lars Porth},
title = {Masking in Fine-Grained Leakage Models: Construction, Implementation
and Verification},
journal = {{IACR} Cryptol. ePrint Arch.},
pages = {603},
year = {2020},
url = {https://eprint.iacr.org/2020/603},
timestamp = {Wed, 27 May 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/iacr/BartheGGOPP20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iacr/BartheCGKLOPRS20,
author = {Gilles Barthe and
Sunjay Cauligi and
Benjamin Gr{\'{e}}goire and
Adrien Koutsos and
Kevin Liao and
Tiago Oliveira and
Swarn Priya and
Tamara Rezk and
Peter Schwabe},
title = {High-Assurance Cryptography Software in the Spectre Era},
journal = {{IACR} Cryptol. ePrint Arch.},
pages = {1104},
year = {2020},
url = {https://eprint.iacr.org/2020/1104},
timestamp = {Wed, 30 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/iacr/BartheCGKLOPRS20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ccs/AlmeidaBBCCGPPS19,
author = {Jos{\'{e}} Bacelar Almeida and
Manuel Barbosa and
Gilles Barthe and
Matthew Campagna and
Ernie Cohen and
Benjamin Gr{\'{e}}goire and
Vitor Pereira and
Bernardo Portela and
Pierre{-}Yves Strub and
Serdar Tasiran},
editor = {Lorenzo Cavallaro and
Johannes Kinder and
XiaoFeng Wang and
Jonathan Katz},
title = {A Machine-Checked Proof of Security for {AWS} Key Management Service},
booktitle = {Proceedings of the 2019 {ACM} {SIGSAC} Conference on Computer and
Communications Security, {CCS} 2019, London, UK, November 11-15, 2019},
pages = {63--78},
publisher = {{ACM}},
year = {2019},
url = {https://doi.org/10.1145/3319535.3354228},
doi = {10.1145/3319535.3354228},
timestamp = {Fri, 29 Apr 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/ccs/AlmeidaBBCCGPPS19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ccs/AlmeidaBBBDGL0S19,
author = {Jos{\'{e}} Bacelar Almeida and
C{\'{e}}cile Baritel{-}Ruet and
Manuel Barbosa and
Gilles Barthe and
Fran{\c{c}}ois Dupressoir and
Benjamin Gr{\'{e}}goire and
Vincent Laporte and
Tiago Oliveira and
Alley Stoughton and
Pierre{-}Yves Strub},
editor = {Lorenzo Cavallaro and
Johannes Kinder and
XiaoFeng Wang and
Jonathan Katz},
title = {Machine-Checked Proofs for Cryptographic Standards: Indifferentiability
of Sponge and Secure High-Assurance Implementations of {SHA-3}},
booktitle = {Proceedings of the 2019 {ACM} {SIGSAC} Conference on Computer and
Communications Security, {CCS} 2019, London, UK, November 11-15, 2019},
pages = {1607--1622},
publisher = {{ACM}},
year = {2019},
url = {https://doi.org/10.1145/3319535.3363211},
doi = {10.1145/3319535.3363211},
timestamp = {Mon, 29 Mar 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/ccs/AlmeidaBBBDGL0S19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/csfw/BartheGJKS19,
author = {Gilles Barthe and
Benjamin Gr{\'{e}}goire and
Charlie Jacomme and
Steve Kremer and
Pierre{-}Yves Strub},
title = {Symbolic Methods in Computational Cryptography Proofs},
booktitle = {32nd {IEEE} Computer Security Foundations Symposium, {CSF} 2019, Hoboken,
NJ, USA, June 25-28, 2019},
pages = {136--151},
publisher = {{IEEE}},
year = {2019},
url = {https://doi.org/10.1109/CSF.2019.00017},
doi = {10.1109/CSF.2019.00017},
timestamp = {Wed, 16 Oct 2019 14:14:49 +0200},
biburl = {https://dblp.org/rec/conf/csfw/BartheGJKS19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/esorics/BartheBCFGS19,
author = {Gilles Barthe and
Sonia Bela{\"{\i}}d and
Ga{\"{e}}tan Cassiers and
Pierre{-}Alain Fouque and
Benjamin Gr{\'{e}}goire and
Fran{\c{c}}ois{-}Xavier Standaert},
editor = {Kazue Sako and
Steve A. Schneider and
Peter Y. A. Ryan},
title = {maskVerif: Automated Verification of Higher-Order Masking in Presence
of Physical Defaults},
booktitle = {Computer Security - {ESORICS} 2019 - 24th European Symposium on Research
in Computer Security, Luxembourg, September 23-27, 2019, Proceedings,
Part {I}},
series = {Lecture Notes in Computer Science},
volume = {11735},
pages = {300--318},
publisher = {Springer},
year = {2019},
url = {https://doi.org/10.1007/978-3-030-29959-0\_15},
doi = {10.1007/978-3-030-29959-0\_15},
timestamp = {Thu, 14 Oct 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/esorics/BartheBCFGS19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/pldi/CauligiSJBWRGBJ19,
author = {Sunjay Cauligi and
Gary Soeller and
Brian Johannesmeyer and
Fraser Brown and
Riad S. Wahby and
John Renner and
Benjamin Gr{\'{e}}goire and
Gilles Barthe and
Ranjit Jhala and
Deian Stefan},
editor = {Kathryn S. McKinley and
Kathleen Fisher},
title = {FaCT: a {DSL} for timing-sensitive computation},
booktitle = {Proceedings of the 40th {ACM} {SIGPLAN} Conference on Programming
Language Design and Implementation, {PLDI} 2019, Phoenix, AZ, USA,
June 22-26, 2019},
pages = {174--189},
publisher = {{ACM}},
year = {2019},
url = {https://doi.org/10.1145/3314221.3314605},
doi = {10.1145/3314221.3314605},
timestamp = {Sun, 09 Jun 2019 18:52:19 +0200},
biburl = {https://dblp.org/rec/conf/pldi/CauligiSJBWRGBJ19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1904-04606,
author = {Jos{\'{e}} Bacelar Almeida and
Manuel Barbosa and
Gilles Barthe and
Benjamin Gr{\'{e}}goire and
Adrien Koutsos and
Vincent Laporte and
Tiago Oliveira and
Pierre{-}Yves Strub},
title = {The Last Mile: High-Assurance and High-Speed Cryptographic Implementations},
journal = {CoRR},
volume = {abs/1904.04606},
year = {2019},
url = {http://arxiv.org/abs/1904.04606},
eprinttype = {arXiv},
eprint = {1904.04606},
timestamp = {Sat, 23 Jan 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-1904-04606.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iacr/BartheBGHLPT19,
author = {Gilles Barthe and
Sandrine Blazy and
Benjamin Gr{\'{e}}goire and
R{\'{e}}mi Hutin and
Vincent Laporte and
David Pichardie and
Alix Trieu},
title = {Formal Verification of a Constant-Time Preserving {C} Compiler},
journal = {{IACR} Cryptol. ePrint Arch.},
pages = {926},
year = {2019},
url = {https://eprint.iacr.org/2019/926},
timestamp = {Mon, 11 May 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/iacr/BartheBGHLPT19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iacr/AlmeidaBBCCGPPS19,
author = {Jos{\'{e}} Bacelar Almeida and
Manuel Barbosa and
Gilles Barthe and
Matthew Campagna and
Ernie Cohen and
Benjamin Gr{\'{e}}goire and
Vitor Pereira and
Bernardo Portela and
Pierre{-}Yves Strub and
Serdar Tasiran},
title = {A Machine-Checked Proof of Security for {AWS} Key Management Service},
journal = {{IACR} Cryptol. ePrint Arch.},
pages = {1042},
year = {2019},
url = {https://eprint.iacr.org/2019/1042},
timestamp = {Fri, 29 Apr 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/iacr/AlmeidaBBCCGPPS19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iacr/AlmeidaBBBDGLOS19,
author = {Jos{\'{e}} Bacelar Almeida and
C{\'{e}}cile Baritel{-}Ruet and
Manuel Barbosa and
Gilles Barthe and
Fran{\c{c}}ois Dupressoir and
Benjamin Gr{\'{e}}goire and
Vincent Laporte and
Tiago Oliveira and
Alley Stoughton and
Pierre{-}Yves Strub},
title = {Machine-Checked Proofs for Cryptographic Standards},
journal = {{IACR} Cryptol. ePrint Arch.},
pages = {1155},
year = {2019},
url = {https://eprint.iacr.org/2019/1155},
timestamp = {Mon, 29 Mar 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/iacr/AlmeidaBBBDGLOS19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/pacmpl/BartheEGHS18,
author = {Gilles Barthe and
Thomas Espitau and
Benjamin Gr{\'{e}}goire and
Justin Hsu and
Pierre{-}Yves Strub},
title = {Proving expected sensitivity of probabilistic programs},
journal = {Proc. {ACM} Program. Lang.},
volume = {2},
number = {{POPL}},
pages = {57:1--57:29},
year = {2018},
url = {https://doi.org/10.1145/3158145},
doi = {10.1145/3158145},
timestamp = {Wed, 17 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/pacmpl/BartheEGHS18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ccs/BartheFGGJS18,
author = {Gilles Barthe and
Xiong Fan and
Joshua Gancher and
Benjamin Gr{\'{e}}goire and
Charlie Jacomme and
Elaine Shi},
editor = {David Lie and
Mohammad Mannan and
Michael Backes and
XiaoFeng Wang},
title = {Symbolic Proofs for Lattice-Based Cryptography},
booktitle = {Proceedings of the 2018 {ACM} {SIGSAC} Conference on Computer and
Communications Security, {CCS} 2018, Toronto, ON, Canada, October
15-19, 2018},
pages = {538--555},
publisher = {{ACM}},
year = {2018},
url = {https://doi.org/10.1145/3243734.3243825},
doi = {10.1145/3243734.3243825},
timestamp = {Tue, 10 Nov 2020 20:00:51 +0100},
biburl = {https://dblp.org/rec/conf/ccs/BartheFGGJS18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cosade/GregoirePSS18,
author = {Benjamin Gr{\'{e}}goire and
Kostas Papagiannopoulos and
Peter Schwabe and
Ko Stoffelen},
editor = {Junfeng Fan and
Benedikt Gierlichs},
title = {Vectorizing Higher-Order Masking},
booktitle = {Constructive Side-Channel Analysis and Secure Design - 9th International
Workshop, {COSADE} 2018, Singapore, April 23-24, 2018, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {10815},
pages = {23--43},
publisher = {Springer},
year = {2018},
url = {https://doi.org/10.1007/978-3-319-89641-0\_2},
doi = {10.1007/978-3-319-89641-0\_2},
timestamp = {Tue, 14 May 2019 10:00:39 +0200},
biburl = {https://dblp.org/rec/conf/cosade/GregoirePSS18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/csfw/Baritel-RuetDFG18,
author = {C{\'{e}}cile Baritel{-}Ruet and
Fran{\c{c}}ois Dupressoir and
Pierre{-}Alain Fouque and
Benjamin Gr{\'{e}}goire},
title = {Formal Security Proof of {CMAC} and Its Variants},
booktitle = {31st {IEEE} Computer Security Foundations Symposium, {CSF} 2018, Oxford,
United Kingdom, July 9-12, 2018},
pages = {91--104},
publisher = {{IEEE} Computer Society},
year = {2018},
url = {https://doi.org/10.1109/CSF.2018.00014},
doi = {10.1109/CSF.2018.00014},
timestamp = {Sun, 12 Nov 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/csfw/Baritel-RuetDFG18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/csfw/BartheGL18,
author = {Gilles Barthe and
Benjamin Gr{\'{e}}goire and
Vincent Laporte},
title = {Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic
"Constant-Time"},
booktitle = {31st {IEEE} Computer Security Foundations Symposium, {CSF} 2018, Oxford,
United Kingdom, July 9-12, 2018},
pages = {328--343},
publisher = {{IEEE} Computer Society},
year = {2018},
url = {https://doi.org/10.1109/CSF.2018.00031},
doi = {10.1109/CSF.2018.00031},
timestamp = {Fri, 24 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/csfw/BartheGL18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/esop/BartheEGGHS18,
author = {Gilles Barthe and
Thomas Espitau and
Marco Gaboardi and
Benjamin Gr{\'{e}}goire and
Justin Hsu and
Pierre{-}Yves Strub},
editor = {Amal Ahmed},
title = {An Assertion-Based Program Logic for Probabilistic Programs},
booktitle = {Programming Languages and Systems - 27th European Symposium on Programming,
{ESOP} 2018, Held as Part of the European Joint Conferences on Theory
and Practice of Software, {ETAPS} 2018, Thessaloniki, Greece, April
14-20, 2018, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {10801},
pages = {117--144},
publisher = {Springer},
year = {2018},
url = {https://doi.org/10.1007/978-3-319-89884-1\_5},
doi = {10.1007/978-3-319-89884-1\_5},
timestamp = {Tue, 05 Jul 2022 08:30:25 +0200},
biburl = {https://dblp.org/rec/conf/esop/BartheEGGHS18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/eurocrypt/BartheBEFGRT18,
author = {Gilles Barthe and
Sonia Bela{\"{\i}}d and
Thomas Espitau and
Pierre{-}Alain Fouque and
Benjamin Gr{\'{e}}goire and
M{\'{e}}lissa Rossi and
Mehdi Tibouchi},
editor = {Jesper Buus Nielsen and
Vincent Rijmen},
title = {Masking the {GLP} Lattice-Based Signature Scheme at Any Order},
booktitle = {Advances in Cryptology - {EUROCRYPT} 2018 - 37th Annual International
Conference on the Theory and Applications of Cryptographic Techniques,
Tel Aviv, Israel, April 29 - May 3, 2018 Proceedings, Part {II}},
series = {Lecture Notes in Computer Science},
volume = {10821},
pages = {354--384},
publisher = {Springer},
year = {2018},
url = {https://doi.org/10.1007/978-3-319-78375-8\_12},
doi = {10.1007/978-3-319-78375-8\_12},
timestamp = {Tue, 29 Dec 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/eurocrypt/BartheBEFGRT18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1803-05535,
author = {Gilles Barthe and
Thomas Espitau and
Marco Gaboardi and
Benjamin Gr{\'{e}}goire and
Justin Hsu and
Pierre{-}Yves Strub},
title = {An Assertion-Based Program Logic for Probabilistic Programs},
journal = {CoRR},
volume = {abs/1803.05535},
year = {2018},
url = {http://arxiv.org/abs/1803.05535},
eprinttype = {arXiv},
eprint = {1803.05535},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1803-05535.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iacr/GregoirePSS18,
author = {Benjamin Gr{\'{e}}goire and
Kostas Papagiannopoulos and
Peter Schwabe and
Ko Stoffelen},
title = {Vectorizing Higher-Order Masking},
journal = {{IACR} Cryptol. ePrint Arch.},
pages = {173},
year = {2018},
url = {http://eprint.iacr.org/2018/173},
timestamp = {Mon, 11 May 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/iacr/GregoirePSS18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iacr/BartheBEFGRT18,
author = {Gilles Barthe and
Sonia Bela{\"{\i}}d and
Thomas Espitau and
Pierre{-}Alain Fouque and
Benjamin Gr{\'{e}}goire and
M{\'{e}}lissa Rossi and
Mehdi Tibouchi},
title = {Masking the {GLP} Lattice-Based Signature Scheme at Any Order},
journal = {{IACR} Cryptol. ePrint Arch.},
pages = {381},
year = {2018},
url = {https://eprint.iacr.org/2018/381},
timestamp = {Mon, 11 May 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/iacr/BartheBEFGRT18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iacr/BartheBDFGSS18,
author = {Gilles Barthe and
Sonia Bela{\"{\i}}d and
Fran{\c{c}}ois Dupressoir and
Pierre{-}Alain Fouque and
Benjamin Gr{\'{e}}goire and
Fran{\c{c}}ois{-}Xavier Standaert and
Pierre{-}Yves Strub},
title = {Improved Parallel Mask Refreshing Algorithms: Generic Solutions with
Parametrized Non-Interference {\&} Automated Optimizations},
journal = {{IACR} Cryptol. ePrint Arch.},
pages = {505},
year = {2018},
url = {https://eprint.iacr.org/2018/505},
timestamp = {Thu, 21 Jan 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/iacr/BartheBDFGSS18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iacr/BartheBFG18,
author = {Gilles Barthe and
Sonia Bela{\"{\i}}d and
Pierre{-}Alain Fouque and
Benjamin Gr{\'{e}}goire},
title = {maskVerif: a formal tool for analyzing software and hardware masked
implementations},
journal = {{IACR} Cryptol. ePrint Arch.},
pages = {562},
year = {2018},
url = {https://eprint.iacr.org/2018/562},
timestamp = {Mon, 11 May 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/iacr/BartheBFG18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iacr/BartheFGGJS18,
author = {Gilles Barthe and
Xiong Fan and
Joshua Gancher and
Benjamin Gr{\'{e}}goire and
Charlie Jacomme and
Elaine Shi},
title = {Symbolic Proofs for Lattice-Based Cryptography},
journal = {{IACR} Cryptol. ePrint Arch.},
pages = {765},
year = {2018},
url = {https://eprint.iacr.org/2018/765},
timestamp = {Mon, 11 May 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/iacr/BartheFGGJS18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ccs/AlmeidaBBBGLOPS17,
author = {Jos{\'{e}} Bacelar Almeida and
Manuel Barbosa and
Gilles Barthe and
Arthur Blot and
Benjamin Gr{\'{e}}goire and
Vincent Laporte and
Tiago Oliveira and
Hugo Pacheco and
Benedikt Schmidt and
Pierre{-}Yves Strub},
editor = {Bhavani Thuraisingham and
David Evans and
Tal Malkin and
Dongyan Xu},
title = {Jasmin: High-Assurance and High-Speed Cryptography},
booktitle = {Proceedings of the 2017 {ACM} {SIGSAC} Conference on Computer and
Communications Security, {CCS} 2017, Dallas, TX, USA, October 30 -
November 03, 2017},
pages = {1807--1823},
publisher = {{ACM}},
year = {2017},
url = {https://doi.org/10.1145/3133956.3134078},
doi = {10.1145/3133956.3134078},
timestamp = {Wed, 29 Jun 2022 15:37:41 +0200},
biburl = {https://dblp.org/rec/conf/ccs/AlmeidaBBBGLOPS17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ccs/AlmeidaBBDGLP17,
author = {Jos{\'{e}} Bacelar Almeida and
Manuel Barbosa and
Gilles Barthe and
Fran{\c{c}}ois Dupressoir and
Benjamin Gr{\'{e}}goire and
Vincent Laporte and
Vitor Pereira},
editor = {Bhavani Thuraisingham and
David Evans and
Tal Malkin and
Dongyan Xu},
title = {A Fast and Verified Software Stack for Secure Function Evaluation},
booktitle = {Proceedings of the 2017 {ACM} {SIGSAC} Conference on Computer and
Communications Security, {CCS} 2017, Dallas, TX, USA, October 30 -
November 03, 2017},
pages = {1989--2006},
publisher = {{ACM}},
year = {2017},
url = {https://doi.org/10.1145/3133956.3134017},
doi = {10.1145/3133956.3134017},
timestamp = {Fri, 29 Apr 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/ccs/AlmeidaBBDGLP17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/eurocrypt/BartheDFGSS17,
author = {Gilles Barthe and
Fran{\c{c}}ois Dupressoir and
Sebastian Faust and
Benjamin Gr{\'{e}}goire and
Fran{\c{c}}ois{-}Xavier Standaert and
Pierre{-}Yves Strub},
editor = {Jean{-}S{\'{e}}bastien Coron and
Jesper Buus Nielsen},
title = {Parallel Implementations of Masking Schemes and the Bounded Moment
Leakage Model},
booktitle = {Advances in Cryptology - {EUROCRYPT} 2017 - 36th Annual International
Conference on the Theory and Applications of Cryptographic Techniques,
Paris, France, April 30 - May 4, 2017, Proceedings, Part {I}},
series = {Lecture Notes in Computer Science},
volume = {10210},
pages = {535--566},
year = {2017},
url = {https://doi.org/10.1007/978-3-319-56620-7\_19},
doi = {10.1007/978-3-319-56620-7\_19},
timestamp = {Thu, 14 Oct 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/eurocrypt/BartheDFGSS17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lpar/BartheEGHS17,
author = {Gilles Barthe and
Thomas Espitau and
Benjamin Gr{\'{e}}goire and
Justin Hsu and
Pierre{-}Yves Strub},
editor = {Thomas Eiter and
David Sands},
title = {Proving uniformity and independence by self-composition and coupling},
booktitle = {LPAR-21, 21st International Conference on Logic for Programming, Artificial
Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017},
series = {EPiC Series in Computing},
volume = {46},
pages = {385--403},
publisher = {EasyChair},
year = {2017},
url = {https://doi.org/10.29007/vz48},
doi = {10.29007/VZ48},
timestamp = {Thu, 14 Oct 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/lpar/BartheEGHS17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/popl/BartheGHS17,
author = {Gilles Barthe and
Benjamin Gr{\'{e}}goire and
Justin Hsu and
Pierre{-}Yves Strub},
editor = {Giuseppe Castagna and
Andrew D. Gordon},
title = {Coupling proofs are probabilistic product programs},
booktitle = {Proceedings of the 44th {ACM} {SIGPLAN} Symposium on Principles of
Programming Languages, {POPL} 2017, Paris, France, January 18-20,
2017},
pages = {161--174},
publisher = {{ACM}},
year = {2017},
url = {https://doi.org/10.1145/3009837.3009896},
doi = {10.1145/3009837.3009896},
timestamp = {Mon, 05 Feb 2024 20:33:37 +0100},
biburl = {https://dblp.org/rec/conf/popl/BartheGHS17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/BartheEGHS17,
author = {Gilles Barthe and
Thomas Espitau and
Benjamin Gr{\'{e}}goire and
Justin Hsu and
Pierre{-}Yves Strub},
title = {Proving uniformity and independence by self-composition and coupling},
journal = {CoRR},
volume = {abs/1701.06477},
year = {2017},
url = {http://arxiv.org/abs/1701.06477},
eprinttype = {arXiv},
eprint = {1701.06477},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/BartheEGHS17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1708-02537,
author = {Gilles Barthe and
Thomas Espitau and
Benjamin Gr{\'{e}}goire and
Justin Hsu and
Pierre{-}Yves Strub},
title = {Proving Expected Sensitivity of Probabilistic Programs},
journal = {CoRR},
volume = {abs/1708.02537},
year = {2017},
url = {http://arxiv.org/abs/1708.02537},
eprinttype = {arXiv},
eprint = {1708.02537},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1708-02537.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iacr/AlmeidaBBDGLP17,
author = {Jos{\'{e}} Bacelar Almeida and
Manuel Barbosa and
Gilles Barthe and
Fran{\c{c}}ois Dupressoir and
Benjamin Gr{\'{e}}goire and
Vincent Laporte and
Vitor Pereira},
title = {A Fast and Verified Software Stack for Secure Function Evaluation},
journal = {{IACR} Cryptol. ePrint Arch.},
pages = {821},
year = {2017},
url = {http://eprint.iacr.org/2017/821},
timestamp = {Fri, 29 Apr 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/iacr/AlmeidaBBDGLP17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iacr/BartheDG17,
author = {Gilles Barthe and
Fran{\c{c}}ois Dupressoir and
Benjamin Gr{\'{e}}goire},
title = {A Note on 'Further Improving Efficiency of Higher-Order Masking Scheme
by Decreasing Randomness Complexity'},
journal = {{IACR} Cryptol. ePrint Arch.},
pages = {1053},
year = {2017},
url = {http://eprint.iacr.org/2017/1053},
timestamp = {Mon, 11 May 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/iacr/BartheDG17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iacr/BartheGL17,
author = {Gilles Barthe and
Benjamin Gr{\'{e}}goire and
Vincent Laporte},
title = {Provably secure compilation of side-channel countermeasures},
journal = {{IACR} Cryptol. ePrint Arch.},
pages = {1233},
year = {2017},
url = {http://eprint.iacr.org/2017/1233},
timestamp = {Mon, 11 May 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/iacr/BartheGL17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ccs/BartheFGGHS16,
author = {Gilles Barthe and
No{\'{e}}mie Fong and
Marco Gaboardi and
Benjamin Gr{\'{e}}goire and
Justin Hsu and
Pierre{-}Yves Strub},
editor = {Edgar R. Weippl and
Stefan Katzenbeisser and
Christopher Kruegel and
Andrew C. Myers and
Shai Halevi},
title = {Advanced Probabilistic Couplings for Differential Privacy},
booktitle = {Proceedings of the 2016 {ACM} {SIGSAC} Conference on Computer and
Communications Security, Vienna, Austria, October 24-28, 2016},
pages = {55--67},
publisher = {{ACM}},
year = {2016},
url = {https://doi.org/10.1145/2976749.2978391},
doi = {10.1145/2976749.2978391},
timestamp = {Tue, 10 Nov 2020 20:00:49 +0100},
biburl = {https://dblp.org/rec/conf/ccs/BartheFGGHS16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ccs/BartheBDFGSZ16,
author = {Gilles Barthe and
Sonia Bela{\"{\i}}d and
Fran{\c{c}}ois Dupressoir and
Pierre{-}Alain Fouque and
Benjamin Gr{\'{e}}goire and
Pierre{-}Yves Strub and
R{\'{e}}becca Zucchini},
editor = {Edgar R. Weippl and
Stefan Katzenbeisser and
Christopher Kruegel and
Andrew C. Myers and
Shai Halevi},
title = {Strong Non-Interference and Type-Directed Higher-Order Masking},
booktitle = {Proceedings of the 2016 {ACM} {SIGSAC} Conference on Computer and
Communications Security, Vienna, Austria, October 24-28, 2016},
pages = {116--129},
publisher = {{ACM}},
year = {2016},
url = {https://doi.org/10.1145/2976749.2978427},
doi = {10.1145/2976749.2978427},
timestamp = {Tue, 10 Nov 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/ccs/BartheBDFGSZ16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/icalp/BartheGGHS16,
author = {Gilles Barthe and
Marco Gaboardi and
Benjamin Gr{\'{e}}goire and
Justin Hsu and
Pierre{-}Yves Strub},
editor = {Ioannis Chatzigiannakis and
Michael Mitzenmacher and
Yuval Rabani and
Davide Sangiorgi},
title = {A Program Logic for Union Bounds},
booktitle = {43rd International Colloquium on Automata, Languages, and Programming,
{ICALP} 2016, July 11-15, 2016, Rome, Italy},
series = {LIPIcs},
volume = {55},
pages = {107:1--107:15},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2016},
url = {https://doi.org/10.4230/LIPIcs.ICALP.2016.107},
doi = {10.4230/LIPICS.ICALP.2016.107},
timestamp = {Mon, 15 Jun 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/icalp/BartheGGHS16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lics/BartheGGHS16,
author = {Gilles Barthe and
Marco Gaboardi and
Benjamin Gr{\'{e}}goire and
Justin Hsu and
Pierre{-}Yves Strub},
editor = {Martin Grohe and
Eric Koskinen and
Natarajan Shankar},
title = {Proving Differential Privacy via Probabilistic Couplings},
booktitle = {Proceedings of the 31st Annual {ACM/IEEE} Symposium on Logic in Computer
Science, {LICS} '16, New York, NY, USA, July 5-8, 2016},
pages = {749--758},
publisher = {{ACM}},
year = {2016},
url = {https://doi.org/10.1145/2933575.2934554},
doi = {10.1145/2933575.2934554},
timestamp = {Wed, 11 Aug 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/lics/BartheGGHS16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/BartheGGHS16,
author = {Gilles Barthe and
Marco Gaboardi and
Benjamin Gr{\'{e}}goire and
Justin Hsu and
Pierre{-}Yves Strub},
title = {Proving Differential Privacy via Probabilistic Couplings},
journal = {CoRR},
volume = {abs/1601.05047},
year = {2016},
url = {http://arxiv.org/abs/1601.05047},
eprinttype = {arXiv},
eprint = {1601.05047},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/BartheGGHS16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/BartheGGHS16a,
author = {Gilles Barthe and
Marco Gaboardi and
Benjamin Gr{\'{e}}goire and
Justin Hsu and
Pierre{-}Yves Strub},
title = {A program logic for union bounds},
journal = {CoRR},
volume = {abs/1602.05681},
year = {2016},
url = {http://arxiv.org/abs/1602.05681},
eprinttype = {arXiv},
eprint = {1602.05681},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/BartheGGHS16a.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/BartheGGHS16b,
author = {Gilles Barthe and
Marco Gaboardi and
Benjamin Gr{\'{e}}goire and
Justin Hsu and
Pierre{-}Yves Strub},
title = {Advanced Probabilistic Couplings for Differential Privacy},
journal = {CoRR},
volume = {abs/1606.07143},
year = {2016},
url = {http://arxiv.org/abs/1606.07143},
eprinttype = {arXiv},
eprint = {1606.07143},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/BartheGGHS16b.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/BartheGHS16,
author = {Gilles Barthe and
Benjamin Gr{\'{e}}goire and
Justin Hsu and
Pierre{-}Yves Strub},
title = {Coupling proofs are probabilistic product programs},
journal = {CoRR},
volume = {abs/1607.03455},
year = {2016},
url = {http://arxiv.org/abs/1607.03455},
eprinttype = {arXiv},
eprint = {1607.03455},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/BartheGHS16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iacr/BartheDFGSS16,
author = {Gilles Barthe and
Fran{\c{c}}ois Dupressoir and
Sebastian Faust and
Benjamin Gr{\'{e}}goire and
Fran{\c{c}}ois{-}Xavier Standaert and
Pierre{-}Yves Strub},
title = {Parallel Implementations of Masking Schemes and the Bounded Moment
Leakage Model},
journal = {{IACR} Cryptol. ePrint Arch.},
pages = {912},
year = {2016},
url = {http://eprint.iacr.org/2016/912},
timestamp = {Mon, 11 May 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/iacr/BartheDFGSS16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ccs/BartheGS15,
author = {Gilles Barthe and
Benjamin Gr{\'{e}}goire and
Benedikt Schmidt},
editor = {Indrajit Ray and
Ninghui Li and
Christopher Kruegel},
title = {Automated Proofs of Pairing-Based Cryptography},
booktitle = {Proceedings of the 22nd {ACM} {SIGSAC} Conference on Computer and
Communications Security, Denver, CO, USA, October 12-16, 2015},
pages = {1156--1168},
publisher = {{ACM}},
year = {2015},
url = {https://doi.org/10.1145/2810103.2813697},
doi = {10.1145/2810103.2813697},
timestamp = {Tue, 10 Nov 2020 19:58:09 +0100},
biburl = {https://dblp.org/rec/conf/ccs/BartheGS15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/eurocrypt/BartheBDFGS15,
author = {Gilles Barthe and
Sonia Bela{\"{\i}}d and
Fran{\c{c}}ois Dupressoir and
Pierre{-}Alain Fouque and
Benjamin Gr{\'{e}}goire and
Pierre{-}Yves Strub},
editor = {Elisabeth Oswald and
Marc Fischlin},
title = {Verified Proofs of Higher-Order Masking},
booktitle = {Advances in Cryptology - {EUROCRYPT} 2015 - 34th Annual International
Conference on the Theory and Applications of Cryptographic Techniques,
Sofia, Bulgaria, April 26-30, 2015, Proceedings, Part {I}},
series = {Lecture Notes in Computer Science},
volume = {9056},
pages = {457--485},
publisher = {Springer},
year = {2015},
url = {https://doi.org/10.1007/978-3-662-46800-5\_18},
doi = {10.1007/978-3-662-46800-5\_18},
timestamp = {Sun, 12 Nov 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/eurocrypt/BartheBDFGS15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lpar/BartheEGHSS15,
author = {Gilles Barthe and
Thomas Espitau and
Benjamin Gr{\'{e}}goire and
Justin Hsu and
L{\'{e}}o Stefanesco and
Pierre{-}Yves Strub},
editor = {Martin Davis and
Ansgar Fehnker and
Annabelle McIver and
Andrei Voronkov},
title = {Relational Reasoning via Probabilistic Coupling},
booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning - 20th
International Conference, {LPAR-20} 2015, Suva, Fiji, November 24-28,
2015, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9450},
pages = {387--401},
publisher = {Springer},
year = {2015},
url = {https://doi.org/10.1007/978-3-662-48899-7\_27},
doi = {10.1007/978-3-662-48899-7\_27},
timestamp = {Mon, 03 Jan 2022 22:31:30 +0100},
biburl = {https://dblp.org/rec/conf/lpar/BartheEGHSS15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/BartheEGHSS15,
author = {Gilles Barthe and
Thomas Espitau and
Benjamin Gr{\'{e}}goire and
Justin Hsu and
L{\'{e}}o Stefanesco and
Pierre{-}Yves Strub},
title = {Relational reasoning via probabilistic coupling},
journal = {CoRR},
volume = {abs/1509.03476},
year = {2015},
url = {http://arxiv.org/abs/1509.03476},
eprinttype = {arXiv},
eprint = {1509.03476},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/BartheEGHSS15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iacr/BartheBDFGS15,
author = {Gilles Barthe and
Sonia Bela{\"{\i}}d and
Fran{\c{c}}ois Dupressoir and
Pierre{-}Alain Fouque and
Benjamin Gr{\'{e}}goire and
Pierre{-}Yves Strub},
title = {Verified Proofs of Higher-Order Masking},
journal = {{IACR} Cryptol. ePrint Arch.},
pages = {60},
year = {2015},
url = {http://eprint.iacr.org/2015/060},
timestamp = {Mon, 11 May 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/iacr/BartheBDFGS15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iacr/BartheBDFG15,
author = {Gilles Barthe and
Sonia Bela{\"{\i}}d and
Fran{\c{c}}ois Dupressoir and
Pierre{-}Alain Fouque and
Benjamin Gr{\'{e}}goire},
title = {Compositional Verification of Higher-Order Masking: Application to
a Verifying Masking Compiler},
journal = {{IACR} Cryptol. ePrint Arch.},
pages = {506},
year = {2015},
url = {http://eprint.iacr.org/2015/506},
timestamp = {Mon, 11 May 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/iacr/BartheBDFG15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ccs/BartheDFGZ14,
author = {Gilles Barthe and
Fran{\c{c}}ois Dupressoir and
Pierre{-}Alain Fouque and
Benjamin Gr{\'{e}}goire and
Jean{-}Christophe Zapalowicz},
editor = {Gail{-}Joon Ahn and
Moti Yung and
Ninghui Li},
title = {Synthesis of Fault Attacks on Cryptographic Implementations},
booktitle = {Proceedings of the 2014 {ACM} {SIGSAC} Conference on Computer and
Communications Security, Scottsdale, AZ, USA, November 3-7, 2014},
pages = {1016--1027},
publisher = {{ACM}},
year = {2014},
url = {https://doi.org/10.1145/2660267.2660304},
doi = {10.1145/2660267.2660304},
timestamp = {Tue, 10 Nov 2020 20:00:23 +0100},
biburl = {https://dblp.org/rec/conf/ccs/BartheDFGZ14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ches/BartheDFGTZ14,
author = {Gilles Barthe and
Fran{\c{c}}ois Dupressoir and
Pierre{-}Alain Fouque and
Benjamin Gr{\'{e}}goire and
Mehdi Tibouchi and
Jean{-}Christophe Zapalowicz},
editor = {Lejla Batina and
Matthew Robshaw},
title = {Making {RSA-PSS} Provably Secure against Non-random Faults},
booktitle = {Cryptographic Hardware and Embedded Systems - {CHES} 2014 - 16th International
Workshop, Busan, South Korea, September 23-26, 2014. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8731},
pages = {206--222},
publisher = {Springer},
year = {2014},
url = {https://doi.org/10.1007/978-3-662-44709-3\_12},
doi = {10.1007/978-3-662-44709-3\_12},
timestamp = {Tue, 14 May 2019 10:00:47 +0200},
biburl = {https://dblp.org/rec/conf/ches/BartheDFGTZ14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/csfw/AkinyeleBGSS14,
author = {Joseph A. Akinyele and
Gilles Barthe and
Benjamin Gr{\'{e}}goire and
Benedikt Schmidt and
Pierre{-}Yves Strub},
title = {Certified Synthesis of Efficient Batch Verifiers},
booktitle = {{IEEE} 27th Computer Security Foundations Symposium, {CSF} 2014, Vienna,
Austria, 19-22 July, 2014},
pages = {153--165},
publisher = {{IEEE} Computer Society},
year = {2014},
url = {https://doi.org/10.1109/CSF.2014.19},
doi = {10.1109/CSF.2014.19},
timestamp = {Fri, 24 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/csfw/AkinyeleBGSS14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/popl/BartheFGSSB14,
author = {Gilles Barthe and
C{\'{e}}dric Fournet and
Benjamin Gr{\'{e}}goire and
Pierre{-}Yves Strub and
Nikhil Swamy and
Santiago Zanella B{\'{e}}guelin},
editor = {Suresh Jagannathan and
Peter Sewell},
title = {Probabilistic relational verification for cryptographic implementations},
booktitle = {The 41st Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of
Programming Languages, {POPL} '14, San Diego, CA, USA, January 20-21,
2014},
pages = {193--206},
publisher = {{ACM}},
year = {2014},
url = {https://doi.org/10.1145/2535838.2535847},
doi = {10.1145/2535838.2535847},
timestamp = {Thu, 24 Jun 2021 16:19:31 +0200},
biburl = {https://dblp.org/rec/conf/popl/BartheFGSSB14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iacr/BartheDFGTZ14,
author = {Gilles Barthe and
Fran{\c{c}}ois Dupressoir and
Pierre{-}Alain Fouque and
Benjamin Gr{\'{e}}goire and
Mehdi Tibouchi and
Jean{-}Christophe Zapalowicz},
title = {Making {RSA-PSS} Provably Secure Against Non-Random Faults},
journal = {{IACR} Cryptol. ePrint Arch.},
pages = {252},
year = {2014},
url = {http://eprint.iacr.org/2014/252},
timestamp = {Mon, 11 May 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/iacr/BartheDFGTZ14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iacr/BartheDFGZ14,
author = {Gilles Barthe and
Fran{\c{c}}ois Dupressoir and
Pierre{-}Alain Fouque and
Benjamin Gr{\'{e}}goire and
Jean{-}Christophe Zapalowicz},
title = {Synthesis of Fault Attacks on Cryptographic Implementations},
journal = {{IACR} Cryptol. ePrint Arch.},
pages = {436},
year = {2014},
url = {http://eprint.iacr.org/2014/436},
timestamp = {Mon, 11 May 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/iacr/BartheDFGZ14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iacr/AlmeidaBBDDGS14,
author = {Jos{\'{e}} Bacelar Almeida and
Manuel Barbosa and
Gilles Barthe and
Guillaume Davy and
Fran{\c{c}}ois Dupressoir and
Benjamin Gr{\'{e}}goire and
Pierre{-}Yves Strub},
title = {Verified Implementations for Secure and Verifiable Computation},
journal = {{IACR} Cryptol. ePrint Arch.},
pages = {456},
year = {2014},
url = {http://eprint.iacr.org/2014/456},
timestamp = {Mon, 11 May 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/iacr/AlmeidaBBDDGS14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jcs/BartheGHOB13,
author = {Gilles Barthe and
Benjamin Gr{\'{e}}goire and
Sylvain Heraud and
Federico Olmedo and
Santiago Zanella B{\'{e}}guelin},
title = {Verified indifferentiable hashing into elliptic curves},
journal = {J. Comput. Secur.},
volume = {21},
number = {6},
pages = {881--917},
year = {2013},
url = {https://doi.org/10.3233/JCS-130476},
doi = {10.3233/JCS-130476},
timestamp = {Mon, 28 Aug 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jcs/BartheGHOB13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ccs/BartheCGKLSB13,
author = {Gilles Barthe and
Juan Manuel Crespo and
Benjamin Gr{\'{e}}goire and
C{\'{e}}sar Kunz and
Yassine Lakhnech and
Benedikt Schmidt and
Santiago Zanella B{\'{e}}guelin},
editor = {Ahmad{-}Reza Sadeghi and
Virgil D. Gligor and
Moti Yung},
title = {Fully automated analysis of padding-based encryption in the computational
model},
booktitle = {2013 {ACM} {SIGSAC} Conference on Computer and Communications Security,
CCS'13, Berlin, Germany, November 4-8, 2013},
pages = {1247--1260},
publisher = {{ACM}},
year = {2013},
url = {https://doi.org/10.1145/2508859.2516663},
doi = {10.1145/2508859.2516663},
timestamp = {Tue, 10 Nov 2020 19:58:06 +0100},
biburl = {https://dblp.org/rec/conf/ccs/BartheCGKLSB13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/csfw/BartheDGKB13,
author = {Gilles Barthe and
George Danezis and
Benjamin Gr{\'{e}}goire and
C{\'{e}}sar Kunz and
Santiago Zanella B{\'{e}}guelin},
title = {Verified Computational Differential Privacy with Applications to Smart
Metering},
booktitle = {2013 {IEEE} 26th Computer Security Foundations Symposium, New Orleans,
LA, USA, June 26-28, 2013},
pages = {287--301},
publisher = {{IEEE} Computer Society},
year = {2013},
url = {https://doi.org/10.1109/CSF.2013.26},
doi = {10.1109/CSF.2013.26},
timestamp = {Fri, 24 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/csfw/BartheDGKB13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fosad/BartheDGKSS13,
author = {Gilles Barthe and
Fran{\c{c}}ois Dupressoir and
Benjamin Gr{\'{e}}goire and
C{\'{e}}sar Kunz and
Benedikt Schmidt and
Pierre{-}Yves Strub},
editor = {Alessandro Aldini and
Javier L{\'{o}}pez and
Fabio Martinelli},
title = {EasyCrypt: {A} Tutorial},
booktitle = {Foundations of Security Analysis and Design {VII} - {FOSAD} 2012/2013
Tutorial Lectures},
series = {Lecture Notes in Computer Science},
volume = {8604},
pages = {146--166},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-319-10082-1\_6},
doi = {10.1007/978-3-319-10082-1\_6},
timestamp = {Thu, 29 Aug 2019 08:10:01 +0200},
biburl = {https://dblp.org/rec/conf/fosad/BartheDGKSS13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/BartheGKLB12,
author = {Gilles Barthe and
Benjamin Gr{\'{e}}goire and
C{\'{e}}sar Kunz and
Yassine Lakhnech and
Santiago Zanella B{\'{e}}guelin},
editor = {Chris Hawblitzel and
Dale Miller},
title = {Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs},
booktitle = {Certified Programs and Proofs - Second International Conference, {CPP}
2012, Kyoto, Japan, December 13-15, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7679},
pages = {7--8},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-35308-6\_3},
doi = {10.1007/978-3-642-35308-6\_3},
timestamp = {Wed, 07 Dec 2022 23:14:04 +0100},
biburl = {https://dblp.org/rec/conf/cpp/BartheGKLB12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/csfw/BackesBBGKSB12,
author = {Michael Backes and
Gilles Barthe and
Matthias Berg and
Benjamin Gr{\'{e}}goire and
C{\'{e}}sar Kunz and
Malte Skoruppa and
Santiago Zanella B{\'{e}}guelin},
editor = {Stephen Chong},
title = {Verified Security of Merkle-Damg{\aa}rd},
booktitle = {25th {IEEE} Computer Security Foundations Symposium, {CSF} 2012, Cambridge,
MA, USA, June 25-27, 2012},
pages = {354--368},
publisher = {{IEEE} Computer Society},
year = {2012},
url = {https://doi.org/10.1109/CSF.2012.14},
doi = {10.1109/CSF.2012.14},
timestamp = {Fri, 24 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/csfw/BackesBBGKSB12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/BartheCGKB12,
author = {Gilles Barthe and
Juan Manuel Crespo and
Benjamin Gr{\'{e}}goire and
C{\'{e}}sar Kunz and
Santiago Zanella B{\'{e}}guelin},
editor = {Lennart Beringer and
Amy P. Felty},
title = {Computer-Aided Cryptographic Proofs},
booktitle = {Interactive Theorem Proving - Third International Conference, {ITP}
2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7406},
pages = {11--27},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-32347-8\_2},
doi = {10.1007/978-3-642-32347-8\_2},
timestamp = {Sun, 25 Oct 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/itp/BartheCGKB12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/mpc/BartheGB12,
author = {Gilles Barthe and
Benjamin Gr{\'{e}}goire and
Santiago Zanella B{\'{e}}guelin},
editor = {Jeremy Gibbons and
Pablo Nogueira},
title = {Probabilistic Relational Hoare Logics for Computer-Aided Security
Proofs},
booktitle = {Mathematics of Program Construction - 11th International Conference,
{MPC} 2012, Madrid, Spain, June 25-27, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7342},
pages = {1--6},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-31113-0\_1},
doi = {10.1007/978-3-642-31113-0\_1},
timestamp = {Sun, 25 Oct 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/mpc/BartheGB12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/post/BartheGHOB12,
author = {Gilles Barthe and
Benjamin Gr{\'{e}}goire and
Sylvain Heraud and
Federico Olmedo and
Santiago Zanella B{\'{e}}guelin},
editor = {Pierpaolo Degano and
Joshua D. Guttman},
title = {Verified Indifferentiable Hashing into Elliptic Curves},
booktitle = {Principles of Security and Trust - First International Conference,
{POST} 2012, Held as Part of the European Joint Conferences on Theory
and Practice of Software, {ETAPS} 2012, Tallinn, Estonia, March 24
- April 1, 2012, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7215},
pages = {209--228},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-28641-4\_12},
doi = {10.1007/978-3-642-28641-4\_12},
timestamp = {Sun, 25 Oct 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/post/BartheGHOB12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sas/BartheGB12,
author = {Gilles Barthe and
Benjamin Gr{\'{e}}goire and
Santiago Zanella B{\'{e}}guelin},
editor = {Antoine Min{\'{e}} and
David Schmidt},
title = {Computer-Aided Cryptographic Proofs},
booktitle = {Static Analysis - 19th International Symposium, {SAS} 2012, Deauville,
France, September 11-13, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7460},
pages = {1--2},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-33125-1\_1},
doi = {10.1007/978-3-642-33125-1\_1},
timestamp = {Sun, 25 Oct 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/sas/BartheGB12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/ercim/Gregoire12,
author = {Benjamin Gr{\'{e}}goire},
title = {Recent Advances in the Formal Verification of Cryptographic Systems:
Turing's Legacy},
journal = {{ERCIM} News},
volume = {2012},
number = {91},
year = {2012},
url = {http://ercim-news.ercim.eu/en91/special/recent-advances-in-the-formal-verification-of-cryptographic-systems-turings-legacy},
timestamp = {Wed, 22 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/ercim/Gregoire12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iacr/BartheCGKLB12,
author = {Gilles Barthe and
Juan Manuel Crespo and
Benjamin Gr{\'{e}}goire and
C{\'{e}}sar Kunz and
Yassine Lakhnech and
Santiago Zanella B{\'{e}}guelin},
title = {Automated Analysis and Synthesis of Padding-Based Encryption Schemes},
journal = {{IACR} Cryptol. ePrint Arch.},
pages = {695},
year = {2012},
url = {http://eprint.iacr.org/2012/695},
timestamp = {Mon, 11 May 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/iacr/BartheCGKLB12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/fmsd/BlechG11,
author = {Jan Olaf Blech and
Benjamin Gr{\'{e}}goire},
title = {Certifying compilers using higher-order theorem provers as certificate
checkers},
journal = {Formal Methods Syst. Des.},
volume = {38},
number = {1},
pages = {33--61},
year = {2011},
url = {https://doi.org/10.1007/s10703-010-0108-7},
doi = {10.1007/S10703-010-0108-7},
timestamp = {Sun, 22 Oct 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/fmsd/BlechG11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/ArmandFGKTW11,
author = {Micha{\"{e}}l Armand and
Germain Faure and
Benjamin Gr{\'{e}}goire and
Chantal Keller and
Laurent Th{\'{e}}ry and
Benjamin Werner},
editor = {Jean{-}Pierre Jouannaud and
Zhong Shao},
title = {A Modular Integration of {SAT/SMT} Solvers to Coq through Proof Witnesses},
booktitle = {Certified Programs and Proofs - First International Conference, {CPP}
2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7086},
pages = {135--150},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-25379-9\_12},
doi = {10.1007/978-3-642-25379-9\_12},
timestamp = {Thu, 14 Oct 2021 10:14:33 +0200},
biburl = {https://dblp.org/rec/conf/cpp/ArmandFGKTW11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/BoespflugDG11,
author = {Mathieu Boespflug and
Maxime D{\'{e}}n{\`{e}}s and
Benjamin Gr{\'{e}}goire},
editor = {Jean{-}Pierre Jouannaud and
Zhong Shao},
title = {Full Reduction at Full Throttle},
booktitle = {Certified Programs and Proofs - First International Conference, {CPP}
2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7086},
pages = {362--377},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-25379-9\_26},
doi = {10.1007/978-3-642-25379-9\_26},
timestamp = {Thu, 25 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/BoespflugDG11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/crypto/BartheGHB11,
author = {Gilles Barthe and
Benjamin Gr{\'{e}}goire and
Sylvain Heraud and
Santiago Zanella B{\'{e}}guelin},
editor = {Phillip Rogaway},
title = {Computer-Aided Security Proofs for the Working Cryptographer},
booktitle = {Advances in Cryptology - {CRYPTO} 2011 - 31st Annual Cryptology Conference,
Santa Barbara, CA, USA, August 14-18, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6841},
pages = {71--90},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-22792-9\_5},
doi = {10.1007/978-3-642-22792-9\_5},
timestamp = {Tue, 14 May 2019 10:00:48 +0200},
biburl = {https://dblp.org/rec/conf/crypto/BartheGHB11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ctrsa/BartheGLB11,
author = {Gilles Barthe and
Benjamin Gr{\'{e}}goire and
Yassine Lakhnech and
Santiago Zanella B{\'{e}}guelin},
editor = {Aggelos Kiayias},
title = {Beyond Provable Security Verifiable {IND-CCA} Security of {OAEP}},
booktitle = {Topics in Cryptology - {CT-RSA} 2011 - The Cryptographers' Track at
the {RSA} Conference 2011, San Francisco, CA, USA, February 14-18,
2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6558},
pages = {180--196},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-19074-2\_13},
doi = {10.1007/978-3-642-19074-2\_13},
timestamp = {Sun, 25 Oct 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/ctrsa/BartheGLB11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/csfw/BartheHBGH10,
author = {Gilles Barthe and
Daniel Hedin and
Santiago Zanella B{\'{e}}guelin and
Benjamin Gr{\'{e}}goire and
Sylvain Heraud},
title = {A Machine-Checked Formalization of Sigma-Protocols},
booktitle = {Proceedings of the 23rd {IEEE} Computer Security Foundations Symposium,
{CSF} 2010, Edinburgh, United Kingdom, July 17-19, 2010},
pages = {246--260},
publisher = {{IEEE} Computer Society},
year = {2010},
url = {https://doi.org/10.1109/CSF.2010.24},
doi = {10.1109/CSF.2010.24},
timestamp = {Fri, 24 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/csfw/BartheHBGH10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/ArmandGST10,
author = {Micha{\"{e}}l Armand and
Benjamin Gr{\'{e}}goire and
Arnaud Spiwack and
Laurent Th{\'{e}}ry},
editor = {Matt Kaufmann and
Lawrence C. Paulson},
title = {Extending Coq with Imperative Features and Its Application to {SAT}
Verification},
booktitle = {Interactive Theorem Proving, First International Conference, {ITP}
2010, Edinburgh, UK, July 11-14, 2010. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6172},
pages = {83--98},
publisher = {Springer},
year = {2010},
url = {https://doi.org/10.1007/978-3-642-14052-5\_8},
doi = {10.1007/978-3-642-14052-5\_8},
timestamp = {Tue, 14 May 2019 10:00:37 +0200},
biburl = {https://dblp.org/rec/conf/itp/ArmandGST10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/BartheGB10,
author = {Gilles Barthe and
Benjamin Gr{\'{e}}goire and
Santiago Zanella B{\'{e}}guelin},
editor = {Matt Kaufmann and
Lawrence C. Paulson},
title = {Programming Language Techniques for Cryptographic Proofs},
booktitle = {Interactive Theorem Proving, First International Conference, {ITP}
2010, Edinburgh, UK, July 11-14, 2010. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6172},
pages = {115--130},
publisher = {Springer},
year = {2010},
url = {https://doi.org/10.1007/978-3-642-14052-5\_10},
doi = {10.1007/978-3-642-14052-5\_10},
timestamp = {Sun, 25 Oct 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/itp/BartheGB10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lpar/GregoireS10,
author = {Benjamin Gr{\'{e}}goire and
Jorge Luis Sacchini},
editor = {Christian G. Ferm{\"{u}}ller and
Andrei Voronkov},
title = {On Strong Normalization of the Calculus of Constructions with Type-Based
Termination},
booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning - 17th
International Conference, LPAR-17, Yogyakarta, Indonesia, October
10-15, 2010. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6397},
pages = {333--347},
publisher = {Springer},
year = {2010},
url = {https://doi.org/10.1007/978-3-642-16242-8\_24},
doi = {10.1007/978-3-642-16242-8\_24},
timestamp = {Tue, 14 May 2019 10:00:55 +0200},
biburl = {https://dblp.org/rec/conf/lpar/GregoireS10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/toplas/BartheGKR09,
author = {Gilles Barthe and
Benjamin Gr{\'{e}}goire and
C{\'{e}}sar Kunz and
Tamara Rezk},
title = {Certificate translation for optimizing compilers},
journal = {{ACM} Trans. Program. Lang. Syst.},
volume = {31},
number = {5},
pages = {18:1--18:45},
year = {2009},
url = {https://doi.org/10.1145/1538917.1538919},
doi = {10.1145/1538917.1538919},
timestamp = {Sun, 22 Oct 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/toplas/BartheGKR09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/icfem/BartheGHKP09,
author = {Gilles Barthe and
Benjamin Gr{\'{e}}goire and
Sylvain Heraud and
C{\'{e}}sar Kunz and
Anne Pacalet},
editor = {Karin K. Breitman and
Ana Cavalcanti},
title = {Implementing a Direct Method for Certificate Translation},
booktitle = {Formal Methods and Software Engineering, 11th International Conference
on Formal Engineering Methods, {ICFEM} 2009, Rio de Janeiro, Brazil,
December 9-12, 2009. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5885},
pages = {541--560},
publisher = {Springer},
year = {2009},
url = {https://doi.org/10.1007/978-3-642-10373-5\_28},
doi = {10.1007/978-3-642-10373-5\_28},
timestamp = {Mon, 21 Feb 2022 14:40:49 +0100},
biburl = {https://dblp.org/rec/conf/icfem/BartheGHKP09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/popl/BartheGB09,
author = {Gilles Barthe and
Benjamin Gr{\'{e}}goire and
Santiago Zanella B{\'{e}}guelin},
editor = {Zhong Shao and
Benjamin C. Pierce},
title = {Formal certification of code-based cryptographic proofs},
booktitle = {Proceedings of the 36th {ACM} {SIGPLAN-SIGACT} Symposium on Principles
of Programming Languages, {POPL} 2009, Savannah, GA, USA, January
21-23, 2009},
pages = {90--101},
publisher = {{ACM}},
year = {2009},
url = {https://doi.org/10.1145/1480881.1480894},
doi = {10.1145/1480881.1480894},
timestamp = {Fri, 25 Jun 2021 14:48:54 +0200},
biburl = {https://dblp.org/rec/conf/popl/BartheGB09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sp/BeguelinBGO09,
author = {Santiago Zanella B{\'{e}}guelin and
Gilles Barthe and
Benjamin Gr{\'{e}}goire and
Federico Olmedo},
title = {Formally Certifying the Security of Digital Signature Schemes},
booktitle = {30th {IEEE} Symposium on Security and Privacy {(SP} 2009), 17-20 May
2009, Oakland, California, {USA}},
pages = {237--250},
publisher = {{IEEE} Computer Society},
year = {2009},
url = {https://doi.org/10.1109/SP.2009.17},
doi = {10.1109/SP.2009.17},
timestamp = {Thu, 21 Sep 2023 16:14:16 +0200},
biburl = {https://dblp.org/rec/conf/sp/BeguelinBGO09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/adg/GregoirePT08,
author = {Benjamin Gr{\'{e}}goire and
Lo{\"{\i}}c Pottier and
Laurent Th{\'{e}}ry},
editor = {Thomas Sturm and
Christoph Zengler},
title = {Proof Certificates for Algebra and Their Application to Automatic
Geometry Theorem Proving},
booktitle = {Automated Deduction in Geometry - 7th International Workshop, {ADG}
2008, Shanghai, China, September 22-24, 2008. Revised Papers},
series = {Lecture Notes in Computer Science},
volume = {6301},
pages = {42--59},
publisher = {Springer},
year = {2008},
url = {https://doi.org/10.1007/978-3-642-21046-4\_3},
doi = {10.1007/978-3-642-21046-4\_3},
timestamp = {Tue, 14 May 2019 10:00:48 +0200},
biburl = {https://dblp.org/rec/conf/adg/GregoirePT08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/BartheGP08,
author = {Gilles Barthe and
Benjamin Gr{\'{e}}goire and
Mariela Pavlova},
editor = {Alessandro Armando and
Peter Baumgartner and
Gilles Dowek},
title = {Preservation of Proof Obligations from Java to the Java Virtual Machine},
booktitle = {Automated Reasoning, 4th International Joint Conference, {IJCAR} 2008,
Sydney, Australia, August 12-15, 2008, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5195},
pages = {83--99},
publisher = {Springer},
year = {2008},
url = {https://doi.org/10.1007/978-3-540-71070-7\_7},
doi = {10.1007/978-3-540-71070-7\_7},
timestamp = {Tue, 14 May 2019 10:00:39 +0200},
biburl = {https://dblp.org/rec/conf/cade/BartheGP08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/csl/BartheGR08,
author = {Gilles Barthe and
Benjamin Gr{\'{e}}goire and
Colin Riba},
editor = {Michael Kaminski and
Simone Martini},
title = {Type-Based Termination with Sized Products},
booktitle = {Computer Science Logic, 22nd International Workshop, {CSL} 2008, 17th
Annual Conference of the EACSL, Bertinoro, Italy, September 16-19,
2008. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5213},
pages = {493--507},
publisher = {Springer},
year = {2008},
url = {https://doi.org/10.1007/978-3-540-87531-4\_35},
doi = {10.1007/978-3-540-87531-4\_35},
timestamp = {Tue, 14 May 2019 10:00:42 +0200},
biburl = {https://dblp.org/rec/conf/csl/BartheGR08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ifip1-7/BartheGHB08,
author = {Gilles Barthe and
Benjamin Gr{\'{e}}goire and
Sylvain Heraud and
Santiago Zanella B{\'{e}}guelin},
editor = {Pierpaolo Degano and
Joshua D. Guttman and
Fabio Martinelli},
title = {Formal Certification of ElGamal Encryption},
booktitle = {Formal Aspects in Security and Trust, 5th International Workshop,
{FAST} 2008, Malaga, Spain, October 9-10, 2008, Revised Selected Papers},
series = {Lecture Notes in Computer Science},
volume = {5491},
pages = {1--19},
publisher = {Springer},
year = {2008},
url = {https://doi.org/10.1007/978-3-642-01465-9\_1},
doi = {10.1007/978-3-642-01465-9\_1},
timestamp = {Sun, 25 Oct 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/ifip1-7/BartheGHB08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lernet/BartheGR08,
author = {Gilles Barthe and
Benjamin Gr{\'{e}}goire and
Colin Riba},
editor = {Ana Bove and
Lu{\'{\i}}s Soares Barbosa and
Alberto Pardo and
Jorge Sousa Pinto},
title = {A Tutorial on Type-Based Termination},
booktitle = {Language Engineering and Rigorous Software Development, International
LerNet {ALFA} Summer School 2008, Piriapolis, Uruguay, February 24
- March 1, 2008, Revised Tutorial Lectures},
series = {Lecture Notes in Computer Science},
volume = {5520},
pages = {100--152},
publisher = {Springer},
year = {2008},
url = {https://doi.org/10.1007/978-3-642-03153-3\_3},
doi = {10.1007/978-3-642-03153-3\_3},
timestamp = {Thu, 14 Oct 2021 10:43:04 +0200},
biburl = {https://dblp.org/rec/conf/lernet/BartheGR08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/types/BarrasCGHS08,
author = {Bruno Barras and
Pierre Corbineau and
Benjamin Gr{\'{e}}goire and
Hugo Herbelin and
Jorge Luis Sacchini},
editor = {Stefano Berardi and
Ferruccio Damiani and
Ugo de'Liguoro},
title = {A New Elimination Rule for the Calculus of Inductive Constructions},
booktitle = {Types for Proofs and Programs, International Conference, {TYPES} 2008,
Torino, Italy, March 26-29, 2008, Revised Selected Papers},
series = {Lecture Notes in Computer Science},
volume = {5497},
pages = {32--48},
publisher = {Springer},
year = {2008},
url = {https://doi.org/10.1007/978-3-642-02444-3\_3},
doi = {10.1007/978-3-642-02444-3\_3},
timestamp = {Tue, 14 May 2019 10:00:42 +0200},
biburl = {https://dblp.org/rec/conf/types/BarrasCGHS08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fmco/BartheCGJP07,
author = {Gilles Barthe and
Pierre Cr{\'{e}}gut and
Benjamin Gr{\'{e}}goire and
Thomas P. Jensen and
David Pichardie},
editor = {Frank S. de Boer and
Marcello M. Bonsangue and
Susanne Graf and
Willem P. de Roever},
title = {The {MOBIUS} Proof Carrying Code Infrastructure},
booktitle = {Formal Methods for Components and Objects, 6th International Symposium,
{FMCO} 2007, Amsterdam, The Netherlands, October 24-26, 2007, Revised
Lectures},
series = {Lecture Notes in Computer Science},
volume = {5382},
pages = {1--24},
publisher = {Springer},
year = {2007},
url = {https://doi.org/10.1007/978-3-540-92188-2\_1},
doi = {10.1007/978-3-540-92188-2\_1},
timestamp = {Tue, 14 May 2019 10:00:53 +0200},
biburl = {https://dblp.org/rec/conf/fmco/BartheCGJP07.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tgc/GregoireS07,
author = {Benjamin Gr{\'{e}}goire and
Jorge Luis Sacchini},
editor = {Gilles Barthe and
C{\'{e}}dric Fournet},
title = {Combining a Verification Condition Generator for a Bytecode Language
with Static Analyses},
booktitle = {Trustworthy Global Computing, Third Symposium, {TGC} 2007, Sophia-Antipolis,
France, November 5-6, 2007, Revised Selected Papers},
series = {Lecture Notes in Computer Science},
volume = {4912},
pages = {23--40},
publisher = {Springer},
year = {2007},
url = {https://doi.org/10.1007/978-3-540-78663-4\_4},
doi = {10.1007/978-3-540-78663-4\_4},
timestamp = {Sat, 19 Oct 2019 20:09:31 +0200},
biburl = {https://dblp.org/rec/conf/tgc/GregoireS07.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/GregoireT06,
author = {Benjamin Gr{\'{e}}goire and
Laurent Th{\'{e}}ry},
editor = {Ulrich Furbach and
Natarajan Shankar},
title = {A Purely Functional Library for Modular Arithmetic and Its Application
to Certifying Large Prime Numbers},
booktitle = {Automated Reasoning, Third International Joint Conference, {IJCAR}
2006, Seattle, WA, USA, August 17-20, 2006, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {4130},
pages = {423--437},
publisher = {Springer},
year = {2006},
url = {https://doi.org/10.1007/11814771\_36},
doi = {10.1007/11814771\_36},
timestamp = {Tue, 14 May 2019 10:00:39 +0200},
biburl = {https://dblp.org/rec/conf/cade/GregoireT06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/flops/GregoireTW06,
author = {Benjamin Gr{\'{e}}goire and
Laurent Th{\'{e}}ry and
Benjamin Werner},
editor = {Masami Hagiya and
Philip Wadler},
title = {A Computational Approach to Pocklington Certificates in Type Theory},
booktitle = {Functional and Logic Programming, 8th International Symposium, {FLOPS}
2006, Fuji-Susono, Japan, April 24-26, 2006, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {3945},
pages = {97--113},
publisher = {Springer},
year = {2006},
url = {https://doi.org/10.1007/11737414\_8},
doi = {10.1007/11737414\_8},
timestamp = {Tue, 14 May 2019 10:00:53 +0200},
biburl = {https://dblp.org/rec/conf/flops/GregoireTW06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fmco/BartheBCGHLPR06,
author = {Gilles Barthe and
Lilian Burdy and
Julien Charles and
Benjamin Gr{\'{e}}goire and
Marieke Huisman and
Jean{-}Louis Lanet and
Mariela Pavlova and
Antoine Requet},
editor = {Frank S. de Boer and
Marcello M. Bonsangue and
Susanne Graf and
Willem P. de Roever},
title = {{JACK} - {A} Tool for Validation of Security and Behaviour of Java
Applications},
booktitle = {Formal Methods for Components and Objects, 5th International Symposium,
{FMCO} 2006, Amsterdam, The Netherlands, November 7-10, 2006, Revised
Lectures},
series = {Lecture Notes in Computer Science},
volume = {4709},
pages = {152--174},
publisher = {Springer},
year = {2006},
url = {https://doi.org/10.1007/978-3-540-74792-5\_7},
doi = {10.1007/978-3-540-74792-5\_7},
timestamp = {Fri, 09 Apr 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/fmco/BartheBCGHLPR06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lpar/BartheGP06,
author = {Gilles Barthe and
Benjamin Gr{\'{e}}goire and
Fernando Pastawski},
editor = {Miki Hermann and
Andrei Voronkov},
title = {CIC[{\^{}}( {)]:} Type-Based Termination of Recursive Definitions
in the Calculus of Inductive Constructions},
booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning, 13th
International Conference, {LPAR} 2006, Phnom Penh, Cambodia, November
13-17, 2006, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {4246},
pages = {257--271},
publisher = {Springer},
year = {2006},
url = {https://doi.org/10.1007/11916277\_18},
doi = {10.1007/11916277\_18},
timestamp = {Sun, 02 Jun 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/lpar/BartheGP06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sas/BartheGKR06,
author = {Gilles Barthe and
Benjamin Gr{\'{e}}goire and
C{\'{e}}sar Kunz and
Tamara Rezk},
editor = {Kwangkeun Yi},
title = {Certificate Translation for Optimizing Compilers},
booktitle = {Static Analysis, 13th International Symposium, {SAS} 2006, Seoul,
Korea, August 29-31, 2006, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {4134},
pages = {301--317},
publisher = {Springer},
year = {2006},
url = {https://doi.org/10.1007/11823230\_20},
doi = {10.1007/11823230\_20},
timestamp = {Tue, 14 May 2019 10:00:52 +0200},
biburl = {https://dblp.org/rec/conf/sas/BartheGKR06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tgc/BartheBCGHMPPSV06,
author = {Gilles Barthe and
Lennart Beringer and
Pierre Cr{\'{e}}gut and
Benjamin Gr{\'{e}}goire and
Martin Hofmann and
Peter M{\"{u}}ller and
Erik Poll and
Germ{\'{a}}n Puebla and
Ian Stark and
Eric V{\'{e}}tillard},
editor = {Ugo Montanari and
Donald Sannella and
Roberto Bruni},
title = {{MOBIUS:} Mobility, Ubiquity, Security},
booktitle = {Trustworthy Global Computing, Second Symposium, {TGC} 2006, Lucca,
Italy, November 7-9, 2006, Revised Selected Papers},
series = {Lecture Notes in Computer Science},
volume = {4661},
pages = {10--29},
publisher = {Springer},
year = {2006},
url = {https://doi.org/10.1007/978-3-540-75336-0\_2},
doi = {10.1007/978-3-540-75336-0\_2},
timestamp = {Tue, 14 May 2019 10:00:52 +0200},
biburl = {https://dblp.org/rec/conf/tgc/BartheBCGHMPPSV06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cassis/2005,
editor = {Gilles Barthe and
Benjamin Gr{\'{e}}goire and
Marieke Huisman and
Jean{-}Louis Lanet},
title = {Construction and Analysis of Safe, Secure, and Interoperable Smart
Devices, Second International Workshop, {CASSIS} 2005, Nice, France,
March 8-11, 2005, Revised Selected Papers},
series = {Lecture Notes in Computer Science},
volume = {3956},
publisher = {Springer},
year = {2006},
url = {https://doi.org/10.1007/11741060},
doi = {10.1007/11741060},
isbn = {3-540-33689-3},
timestamp = {Fri, 09 Apr 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cassis/2005.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/csl/BarrasG05,
author = {Bruno Barras and
Benjamin Gr{\'{e}}goire},
editor = {C.{-}H. Luke Ong},
title = {On the Role of Type Decorations in the Calculus of Inductive Constructions},
booktitle = {Computer Science Logic, 19th International Workshop, {CSL} 2005, 14th
Annual Conference of the EACSL, Oxford, UK, August 22-25, 2005, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {3634},
pages = {151--166},
publisher = {Springer},
year = {2005},
url = {https://doi.org/10.1007/11538363\_12},
doi = {10.1007/11538363\_12},
timestamp = {Tue, 14 May 2019 10:00:42 +0200},
biburl = {https://dblp.org/rec/conf/csl/BarrasG05.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tlca/BartheGP05,
author = {Gilles Barthe and
Benjamin Gr{\'{e}}goire and
Fernando Pastawski},
editor = {Pawel Urzyczyn},
title = {Practical Inference for Type-Based Termination in a Polymorphic Setting},
booktitle = {Typed Lambda Calculi and Applications, 7th International Conference,
{TLCA} 2005, Nara, Japan, April 21-23, 2005, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {3461},
pages = {71--85},
publisher = {Springer},
year = {2005},
url = {https://doi.org/10.1007/11417170\_7},
doi = {10.1007/11417170\_7},
timestamp = {Sun, 02 Jun 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/tlca/BartheGP05.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tphol/GregoireM05,
author = {Benjamin Gr{\'{e}}goire and
Assia Mahboubi},
editor = {Joe Hurd and
Thomas F. Melham},
title = {Proving Equalities in a Commutative Ring Done Right in Coq},
booktitle = {Theorem Proving in Higher Order Logics, 18th International Conference,
TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {3603},
pages = {98--113},
publisher = {Springer},
year = {2005},
url = {https://doi.org/10.1007/11541868\_7},
doi = {10.1007/11541868\_7},
timestamp = {Tue, 14 May 2019 10:00:48 +0200},
biburl = {https://dblp.org/rec/conf/tphol/GregoireM05.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/types/BertotGL04,
author = {Yves Bertot and
Benjamin Gr{\'{e}}goire and
Xavier Leroy},
editor = {Jean{-}Christophe Filli{\^{a}}tre and
Christine Paulin{-}Mohring and
Benjamin Werner},
title = {A Structured Approach to Proving Compiler Optimizations Based on Dataflow
Analysis},
booktitle = {Types for Proofs and Programs, International Workshop, {TYPES} 2004,
Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers},
series = {Lecture Notes in Computer Science},
volume = {3839},
pages = {66--81},
publisher = {Springer},
year = {2004},
url = {https://doi.org/10.1007/11617990\_5},
doi = {10.1007/11617990\_5},
timestamp = {Tue, 14 May 2019 10:00:42 +0200},
biburl = {https://dblp.org/rec/conf/types/BertotGL04.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/icfp/GregoireL02,
author = {Benjamin Gr{\'{e}}goire and
Xavier Leroy},
editor = {Mitchell Wand and
Simon L. Peyton Jones},
title = {A compiled implementation of strong reduction},
booktitle = {Proceedings of the Seventh {ACM} {SIGPLAN} International Conference
on Functional Programming {(ICFP} '02), Pittsburgh, Pennsylvania,
USA, October 4-6, 2002},
pages = {235--246},
publisher = {{ACM}},
year = {2002},
url = {https://doi.org/10.1145/581478.581501},
doi = {10.1145/581478.581501},
timestamp = {Wed, 07 Jul 2021 17:30:33 +0200},
biburl = {https://dblp.org/rec/conf/icfp/GregoireL02.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
a service of 
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-02-06 23:46 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
