Recherche - Archive ouverte HAL Accéder directement au contenu

Filtrer vos résultats

72 résultats
Page :
triés par
Image document

Full reduction at full throttle

 Mathieu Boespflug , Maxime Dénès , Benjamin Grégoire
Certified Programs and Proofs, Dec 2011, Kenting, Taiwan. ⟨10.1007/978-3-642-25379-9_26⟩
Communication dans un congrès hal-00650940v1
Image document

A Machine-Checked Formalization of Sigma-Protocols

 Gilles Barthe , Daniel Hedin , Santiago Zanella-Béguelin , Benjamin Grégoire , Sylvain Heraud
CSF'10, Jul 2010, Edinburgh, Sweden. pp.246-260, ⟨10.1109/CSF.2010.24⟩
Communication dans un congrès inria-00552886v1

Certified Synthesis of Efficient Batch Verifiers

 Joseph A. Akinyele , Gilles Barthe , Benjamin Grégoire , Benedikt Schmidt , Pierre-Yves Strub
CSF 2014 - IEEE 27th Computer Security Foundations Symposium, Jul 2014, Vienna, Austria. pp.153 - 165, ⟨10.1109/CSF.2014.19⟩
Communication dans un congrès hal-01094565v1
Image document

Masking in Fine-Grained Leakage Models: Construction, Implementation and Verification

 Gilles Barthe , Marc Gourjon , Benjamin Grégoire , Maximilian Orlt , Clara Paglialonga , et al.
IACR Transactions on Cryptographic Hardware and Embedded Systems, 2021, pp.189-228. ⟨10.46586/tches.v2021.i2.189-228⟩
Article dans une revue hal-03528937v1

Structured Leakage and Applications to Cryptographic Constant-Time and Cost

 Gilles Barthe , Benjamin Grégoire , Vincent Laporte , Swarn Priya
CCS 2021 - ACM SIGSAC Conference on Computer and Communications Security, Nov 2021, Virtual Event, South Korea. pp.462-476, ⟨10.1145/3460120.3484761⟩
Communication dans un congrès hal-03430789v1
Image document

A New Elimination Rule for the Calculus of Inductive Constructions

 Bruno Barras , Pierre Corbineau , Benjamin Grégoire , Hugo Herbelin , Jorge Luis Sacchini
Types for Proofs and Programs, Mar 2008, Torino, Italy. pp.32-48, ⟨10.1007/978-3-642-02444-3_3⟩
Communication dans un congrès inria-00524938v1
Image document

Automated Verification of Higher-Order Masking in Presence of Physical Defaults

 Gilles Barthe , Sonia Belaïd , Gaëtan Cassiers , Pierre-Alain Fouque , Benjamin Grégoire , et al.
ESORICS 2019 - 24th European Symposium on Research in Computer Security, Sep 2019, Luxembourg, Luxembourg. pp.300-318, ⟨10.1007/978-3-030-29959-0_15⟩
Communication dans un congrès hal-02404662v1
Image document

A Fast and Verified Software Stack for Secure Function Evaluation

 José Bacelar Almeida , Manuel Barbosa , Gilles Barthe , Francois Dupressoir , Benjamin Grégoire , et al.
CCS 2017 - ACM SIGSAC Conference on Computer and Communications Security, Oct 2017, Dallas, United States. pp.1-18
Communication dans un congrès hal-01649104v1
Image document

A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses

 Michaël Armand , Germain Faure , Benjamin Grégoire , Chantal Keller , Laurent Thery , et al.
CPP - Certified Programs and Proofs - First International Conference - 2011, Dec 2011, Kenting, Taiwan. pp.135-150, ⟨10.1007/978-3-642-25379-9_12⟩
Communication dans un congrès istex hal-00639130v1

Proof Certificates for Algebra and their Application to Automatic Geometry Theorem Proving

 Benjamin Grégoire , Loïc Pottier , Laurent Théry
Thomas Sturm; Christoph Zengler. Automated Deduction in Geometry, 6301, Springer, pp.42-59, 2011, Lecture Notes in Computer Science, 978-3-642-21045-7. ⟨10.1007/978-3-642-21046-4_3⟩
Chapitre d'ouvrage hal-01112767v1

The Last Mile: High-Assurance and High-Speed Cryptographic Implementations

 José Bacelar Almeida , Manuel Barbosa , Gilles Barthe , Benjamin Grégoire , Adrien Koutsos , et al.
SP 2020 - 41st IEEE Symposium on Security and Privacy, May 2020, San Francisco / Virtual, United States. pp.965-982, ⟨10.1109/SP40000.2020.00028⟩
Communication dans un congrès hal-02974993v1
Image document

Improved parallel mask refreshing algorithms: generic solutions with parametrized non-interference and automated optimizations

 Gilles Barthe , Sonia Belaïd , François Dupressoir , Pierre-Alain Fouque , Benjamin Grégoire , et al.
Journal of Cryptographic Engineering, 2020, 10 (1), pp.17-26. ⟨10.1007/s13389-018-00202-2⟩
Article dans une revue hal-03133221v1
Image document

Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3

 José Bacelar Almeida , Cécile Baritel-Ruet , Manuel Barbosa , Gilles Barthe , François Dupressoir , et al.
CCS 2019 - 26th ACM Conference on Computer and Communications Security, Nov 2019, London, United Kingdom. pp.1607-1622, ⟨10.1145/3319535.3363211⟩
Communication dans un congrès hal-02404581v1

EasyCrypt: A Tutorial

 Gilles Barthe , Francois Dupressoir , Benjamin Grégoire , Cesar Kunz , Benedikt Schmidt , et al.
FOSAD 2013, 2013, Bertinoro, Italy. ⟨10.1007/978-3-319-10082-1_6⟩
Communication dans un congrès hal-01114366v1

Enforcing Fine-grained Constant-time Policies

 Basavesh Ammanaghatta Shivakumar , Gilles Barthe , Benjamin Grégoire , Vincent Laporte , Swarn Priya
CCS 2022 - 2022 ACM SIGSAC Conference on Computer and Communications Security, Nov 2022, Los Angeles CA, United States. pp.83-96, ⟨10.1145/3548606.3560689⟩
Communication dans un congrès hal-03844366v1
Image document

Typing High-Speed Cryptography against Spectre v1

 Basavesh Ammanaghatta Shivakumar , Gilles Barthe , Benjamin Grégoire , Vincent Laporte , Tiago Oliveira , et al.
SP 2023- IEEE Symposium on Security and Privacy, IEEE, May 2023, San Francisco, United States. pp.1592-1609, ⟨10.1109/SP46215.2023.10179418⟩
Communication dans un congrès hal-04106448v1
Image document

An Assertion-Based Program Logic for Probabilistic Programs

 Gilles Barthe , Thomas Espitau , Marco Gaboardi , Benjamin Grégoire , Justin Hsu , et al.
Lecture Notes in Computer Science, Apr 2018, Thessaloniki, Greece. pp.117-144, ⟨10.1007/978-3-319-89884-1_5⟩
Communication dans un congrès hal-01959567v1
Image document

High-Assurance Cryptography in the Spectre Era

 Gilles Barthe , Sunjay Cauligi , Benjamin Grégoire , Adrien Koutsos , Kevin Liao , et al.
S&P 2021 - IEEE Symposium of Security and Privacy, May 2021, Virtual, France. ⟨10.1109/SP40001.2021.00046⟩
Communication dans un congrès hal-03352062v1
Image document

Formal Security Proof of CMAC and Its Variants

 Cécile Baritel-Ruet , François Dupressoir , Pierre-Alain Fouque , Benjamin Grégoire
CSF 2018 - 31st EEE Computer Security Foundations Symposium, Jul 2018, Oxford, United Kingdom
Communication dans un congrès hal-01959554v1
Image document

Boolean reflection via type classes

 Benjamin Grégoire , Enrico Tassi
Coq Workshop, Aug 2016, Nancy, France
Communication dans un congrès hal-01410530v1
Image document

Jasmin: High-Assurance and High-Speed Cryptography

 José Bacelar Almeida , Manuel Barbosa , Gilles Barthe , Arthur Blot , Benjamin Grégoire , et al.
CCS 2017 - Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, Oct 2017, Dallas, United States. pp.1-17
Communication dans un congrès hal-01649140v1
Image document

On Strong Normalization of the Calculus of Constructions with Type-Based Termination

 Benjamin Grégoire , Jorge Luis Sacchini
17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Oct 2010, Yogyakarta, Indonesia. pp.333-347, ⟨10.1007/978-3-642-16242-8_24⟩
Communication dans un congrès hal-00537104v1

Verified Computational Differential Privacy with Applications to Smart Metering

 Gilles Barthe , George Danezis , Benjamin Grégoire , César Kunz , Santiago Zanella-Béguelin
2013 IEEE 26th Computer Security Foundations Symposium, Jun 2013, New Orleans, United States. pp.287-301, ⟨10.1109/CSF.2013.26⟩
Communication dans un congrès hal-00935736v1

Verified indifferentiable hashing into elliptic curves

 Gilles Barthe , Benjamin Grégoire , Sylvain Heraud , Federico Olmedo , Santiago Zanella-Béguelin
Journal of Computer Security, 2013
Article dans une revue hal-00935747v1
Image document

Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic “Constant-Time”

 Gilles Barthe , Benjamin Grégoire , Vincent Laporte
CSF 2018 - 31st IEEE Computer Security Foundations Symposium, Jul 2018, Oxford, United Kingdom
Communication dans un congrès hal-01959560v1
Image document

FaCT: A DSL for Timing-Sensitive Computation

 Sunjay Cauligi , Gary Soeller , Brian Johannesmeyer , Fraser Brown , Riad S Wahby , et al.
PLDI 2019 - 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, Jun 2019, Phoenix, United States. ⟨10.1145/3314221.3314605⟩
Communication dans un congrès hal-02404755v1
Image document

Hardware Private Circuits: From Trivial Composition to Full Verification

 Gaetan Cassiers , Benjamin Grégoire , Itamar Levi , Francois-Xavier Standaert
IEEE Transactions on Computers, 2020, ⟨10.1109/tc.2020.3022979⟩
Article dans une revue hal-03133227v1
Image document

Mechanized Proofs of Adversarial Complexity and Application to Universal Composability

 Manuel Barbosa , Gilles Barthe , Benjamin Grégoire , Adrien Koutsos , Pierre-Yves Strub
CCS 2021 - ACM SIGSAC Conference on Computer and Communications Security, Nov 2021, Virtual Event, South Korea. pp.2541-2563, ⟨10.1145/3460120.3484548⟩
Communication dans un congrès hal-03469015v1
Image document

Synthesis of Fault Attacks on Cryptographic Implementations

 Gilles Barthe , François Dupressoir , Pierre-Alain Fouque , Benjamin Grégoire , Jean-Christophe Zapalowicz
ACM CCS 2014, Nov 2014, Scottsdale, United States. pp.16, ⟨10.1145/2660267.2660304⟩
Communication dans un congrès hal-01094034v1
Image document

Security Analysis of ElGamal Implementations

 Mohamad El Laz , Benjamin Grégoire , Tamara Rezk
SECRYPT 2020 - 17th International Conference on Security and Cryptography, Jul 2020, Lieusaint - Paris, France. pp.310-321, ⟨10.5220/0009817103100321⟩
Communication dans un congrès hal-03141511v1
Page :