Vincent Cheval : Publications

On Learning Polynomial Recursive Programs

Alex Buna−Marginean‚ Vincent Cheval‚ Mahsa Shirmohammadi and James Worrell

In Proc. ACM Program. Lang.. Vol. 8. No. POPL. 2024.

To appear January 2024.

Details about On Learning Polynomial Recursive Programs | BibTeX data for On Learning Polynomial Recursive Programs | DOI (10.1145/3632876)

Symbolic protocol verification with dice

Vincent Cheval‚ Raphaëlle Crubillé and Steve Kremer

In J. Comput. Secur.. Vol. 31. No. 5. Pages 501–538. 2023.

Details about Symbolic protocol verification with dice | BibTeX data for Symbolic protocol verification with dice | DOI (10.3233/JCS-230037) | Download (pdf) of Symbolic protocol verification with dice

Hash Gone Bad: Automated discovery of protocol attacks that exploit hash function weaknesses

Vincent Cheval‚ Cas Cremers‚ Alexander Dax‚ Lucca Hirschi‚ Charlie Jacomme and Steve Kremer

In Joseph A. Calandrino and Carmela Troncoso, editors, 32nd USENIX Security Symposium‚ USENIX Security 2023‚ Anaheim‚ CA‚ USA‚ August 9−11‚ 2023. Pages 5899–5916. USENIX Association. 2023.

Distinguish Paper Award

Details about Hash Gone Bad: Automated discovery of protocol attacks that exploit hash function weaknesses | BibTeX data for Hash Gone Bad: Automated discovery of protocol attacks that exploit hash function weaknesses | Download (pdf) of Hash Gone Bad: Automated discovery of protocol attacks that exploit hash function weaknesses

Automatic verification of transparency protocols

Vincent Cheval‚ José Moreira and Mark Ryan

In 8th IEEE European Symposium on Security and Privacy‚ EuroS&P 2023‚ Delft‚ Netherlands‚ July 3−7‚ 2023. Pages 107–121. IEEE. 2023.

Details about Automatic verification of transparency protocols | BibTeX data for Automatic verification of transparency protocols | DOI (10.1109/EUROSP57164.2023.00016) | Download (pdf) of Automatic verification of transparency protocols

Election Verifiability with ProVerif

Vincent Cheval‚ Véronique Cortier and Alexandre Debant

In 36th IEEE Computer Security Foundations Symposium‚ CSF 2023‚ Dubrovnik‚ Croatia‚ July 10−14‚ 2023. Pages 43–58. IEEE. 2023.

Details about Election Verifiability with ProVerif | BibTeX data for Election Verifiability with ProVerif | DOI (10.1109/CSF57540.2023.00032) | Download (pdf) of Election Verifiability with ProVerif

Indistinguishability Beyond Diff−Equivalence in ProVerif

Vincent Cheval and Itsaka Rakotonirina

In 36th IEEE Computer Security Foundations Symposium‚ CSF 2023‚ Dubrovnik‚ Croatia‚ July 10−14‚ 2023. Pages 184–199. IEEE. 2023.

Distinguished paper award

Details about Indistinguishability Beyond Diff−Equivalence in ProVerif | BibTeX data for Indistinguishability Beyond Diff−Equivalence in ProVerif | DOI (10.1109/CSF57540.2023.00036) | Download (pdf) of Indistinguishability Beyond Diff−Equivalence in ProVerif

SAPIC+: protocol verifiers of the world‚ unite!

Vincent Cheval‚ Charlie Jacomme‚ Steve Kremer and Robert Künnemann

In Kevin R. B. Butler and Kurt Thomas, editors, 31st USENIX Security Symposium‚ USENIX Security 2022‚ Boston‚ MA‚ USA‚ August 10−12‚ 2022. Pages 3935–3952. USENIX Association. 2022.

Details about SAPIC+: protocol verifiers of the world‚ unite! | BibTeX data for SAPIC+: protocol verifiers of the world‚ unite! | Link to SAPIC+: protocol verifiers of the world‚ unite!

ProVerif with Lemmas‚ Induction‚ Fast Subsumption‚ and Much More

Bruno Blanchet‚ Vincent Cheval and Véronique Cortier

In 43rd IEEE Symposium on Security and Privacy‚ SP 2022‚ San Francisco‚ CA‚ USA‚ May 22−26‚ 2022. Pages 69–86. IEEE. 2022.

Details about ProVerif with Lemmas‚ Induction‚ Fast Subsumption‚ and Much More | BibTeX data for ProVerif with Lemmas‚ Induction‚ Fast Subsumption‚ and Much More | DOI (10.1109/SP46214.2022.9833653) | Download (pdf) of ProVerif with Lemmas‚ Induction‚ Fast Subsumption‚ and Much More

Symbolic protocol verification with dice: process equivalences in the presence of probabilities

Vincent Cheval‚ Raphaëlle Crubillé and Steve Kremer

In 35th IEEE Computer Security Foundations Symposium‚ CSF 2022‚ Haifa‚ Israel‚ August 7−10‚ 2022. Pages 319–334. IEEE. 2022.

Details about Symbolic protocol verification with dice: process equivalences in the presence of probabilities | BibTeX data for Symbolic protocol verification with dice: process equivalences in the presence of probabilities | DOI (10.1109/CSF54842.2022.9919644) | Download (pdf) of Symbolic protocol verification with dice: process equivalences in the presence of probabilities

A Symbolic Analysis of Privacy for TLS 1.3 with Encrypted Client Hello

Karthikeyan Bhargavan‚ Vincent Cheval and Christopher A. Wood

In Heng Yin‚ Angelos Stavrou‚ Cas Cremers and Elaine Shi, editors, Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security‚ CCS 2022‚ Los Angeles‚ CA‚ USA‚ November 7−11‚ 2022. Pages 365–379. ACM. 2022.

Details about A Symbolic Analysis of Privacy for TLS 1.3 with Encrypted Client Hello | BibTeX data for A Symbolic Analysis of Privacy for TLS 1.3 with Encrypted Client Hello | DOI (10.1145/3548606.3559360) | Download (pdf) of A Symbolic Analysis of Privacy for TLS 1.3 with Encrypted Client Hello

On the semantics of communications when verifying equivalence properties

Kushal Babel‚ Vincent Cheval and Steve Kremer

In J. Comput. Secur.. Vol. 28. No. 1. Pages 71–127. 2020.

Details about On the semantics of communications when verifying equivalence properties | BibTeX data for On the semantics of communications when verifying equivalence properties | DOI (10.3233/JCS-191366) | Download (pdf) of On the semantics of communications when verifying equivalence properties

The Hitchhiker's Guide to Decidability and Complexity of Equivalence Properties in Security Protocols

Vincent Cheval‚ Steve Kremer and Itsaka Rakotonirina

In Vivek Nigam‚ Tajana Ban Kirigin‚ Carolyn L. Talcott‚ Joshua D. Guttman‚ Stepan L. Kuznetsov‚ Boon Thau Loo and Mitsuhiro Okada, editors, Logic‚ Language‚ and Security − Essays Dedicated to Andre Scedrov on the Occasion of His 65th Birthday. Vol. 12300 of Lecture Notes in Computer Science. Pages 127–145. Springer. 2020.

Details about The Hitchhiker's Guide to Decidability and Complexity of Equivalence Properties in Security Protocols | BibTeX data for The Hitchhiker's Guide to Decidability and Complexity of Equivalence Properties in Security Protocols | DOI (10.1007/978-3-030-62077-6_10) | Download (pdf) of The Hitchhiker's Guide to Decidability and Complexity of Equivalence Properties in Security Protocols

Exploiting Symmetries When Proving Equivalence Properties for Security Protocols

Vincent Cheval‚ Steve Kremer and Itsaka Rakotonirina

In Lorenzo Cavallaro‚ Johannes Kinder‚ XiaoFeng Wang and Jonathan Katz, editors, Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security‚ CCS 2019‚ London‚ UK‚ November 11−15‚ 2019. Pages 905–922. ACM. 2019.

Details about Exploiting Symmetries When Proving Equivalence Properties for Security Protocols | BibTeX data for Exploiting Symmetries When Proving Equivalence Properties for Security Protocols | DOI (10.1145/3319535.3354260) | Download (pdf) of Exploiting Symmetries When Proving Equivalence Properties for Security Protocols

DEEPSEC: Deciding Equivalence Properties in Security Protocols Theory and Practice

Vincent Cheval‚ Steve Kremer and Itsaka Rakotonirina

In 2018 IEEE Symposium on Security and Privacy‚ SP 2018‚ Proceedings‚ 21−23 May 2018‚ San Francisco‚ California‚ USA. Pages 529–546. IEEE Computer Society. 2018.

Distinguished paper award

Details about DEEPSEC: Deciding Equivalence Properties in Security Protocols Theory and Practice | BibTeX data for DEEPSEC: Deciding Equivalence Properties in Security Protocols Theory and Practice | DOI (10.1109/SP.2018.00033) | Download (pdf) of DEEPSEC: Deciding Equivalence Properties in Security Protocols Theory and Practice

A Little More Conversation‚ a Little Less Action‚ a Lot More Satisfaction: Global States in ProVerif

Vincent Cheval‚ Véronique Cortier and Mathieu Turuani

In 31st IEEE Computer Security Foundations Symposium‚ CSF 2018‚ Oxford‚ United Kingdom‚ July 9−12‚ 2018. Pages 344–358. IEEE Computer Society. 2018.

Details about A Little More Conversation‚ a Little Less Action‚ a Lot More Satisfaction: Global States in ProVerif | BibTeX data for A Little More Conversation‚ a Little Less Action‚ a Lot More Satisfaction: Global States in ProVerif | DOI (10.1109/CSF.2018.00032) | Download (pdf) of A Little More Conversation‚ a Little Less Action‚ a Lot More Satisfaction: Global States in ProVerif

The DEEPSEC Prover

Vincent Cheval‚ Steve Kremer and Itsaka Rakotonirina

In Hana Chockler and Georg Weissenbacher, editors, Computer Aided Verification − 30th International Conference‚ CAV 2018‚ Held as Part of the Federated Logic Conference‚ FloC 2018‚ Oxford‚ UK‚ July 14−17‚ 2018‚ Proceedings‚ Part II. Vol. 10982 of Lecture Notes in Computer Science. Pages 28–36. Springer. 2018.

Details about The DEEPSEC Prover | BibTeX data for The DEEPSEC Prover | DOI (10.1007/978-3-319-96142-2_4) | Download (pdf) of The DEEPSEC Prover

A procedure for deciding symbolic equivalence between sets of constraint systems

Vincent Cheval‚ Hubert Comon−Lundh and Stéphanie Delaune

In Inf. Comput.. Vol. 255. Pages 94–125. 2017.

Details about A procedure for deciding symbolic equivalence between sets of constraint systems | BibTeX data for A procedure for deciding symbolic equivalence between sets of constraint systems | DOI (10.1016/J.IC.2017.05.004) | Download (pdf) of A procedure for deciding symbolic equivalence between sets of constraint systems

On Communication Models When Verifying Equivalence Properties

Kushal Babel‚ Vincent Cheval and Steve Kremer

In Matteo Maffei and Mark Ryan, editors, Principles of Security and Trust − 6th International Conference‚ POST 2017‚ Held as Part of the European Joint Conferences on Theory and Practice of Software‚ ETAPS 2017‚ Uppsala‚ Sweden‚ April 22−29‚ 2017‚ Proceedings. Vol. 10204 of Lecture Notes in Computer Science. Pages 141–163. Springer. 2017.

Details about On Communication Models When Verifying Equivalence Properties | BibTeX data for On Communication Models When Verifying Equivalence Properties | DOI (10.1007/978-3-662-54455-6_7) | Download (pdf) of On Communication Models When Verifying Equivalence Properties

Secure Composition of PKIs with Public Key Protocols

Vincent Cheval‚ Véronique Cortier and Bogdan Warinschi

In 30th IEEE Computer Security Foundations Symposium‚ CSF 2017‚ Santa Barbara‚ CA‚ USA‚ August 21−25‚ 2017. Pages 144–158. IEEE Computer Society. 2017.

Details about Secure Composition of PKIs with Public Key Protocols | BibTeX data for Secure Composition of PKIs with Public Key Protocols | DOI (10.1109/CSF.2017.28) | Download (pdf) of Secure Composition of PKIs with Public Key Protocols

Automated Verification of Equivalence Properties of Cryptographic Protocols

Rohit Chadha‚ Vincent Cheval‚ Ştefan Ciobâcă and Steve Kremer

In ACM Trans. Comput. Log.. Vol. 17. No. 4. Pages 23. 2016.

Listed in ACM Computing Reviews' 21st Annual Best of Computing list of notable books and articles for 2016

Details about Automated Verification of Equivalence Properties of Cryptographic Protocols | BibTeX data for Automated Verification of Equivalence Properties of Cryptographic Protocols | DOI (10.1145/2926715) | Download (pdf) of Automated Verification of Equivalence Properties of Cryptographic Protocols

DTKI: A New Formalized PKI with Verifiable Trusted Parties

Jiangshan Yu‚ Vincent Cheval and Mark Ryan

In Comput. J.. Vol. 59. No. 11. Pages 1695–1713. 2016.

Details about DTKI: A New Formalized PKI with Verifiable Trusted Parties | BibTeX data for DTKI: A New Formalized PKI with Verifiable Trusted Parties | DOI (10.1093/COMJNL/BXW039) | Download (pdf) of DTKI: A New Formalized PKI with Verifiable Trusted Parties

Composing Security Protocols: From Confidentiality to Privacy

Myrto Arapinis‚ Vincent Cheval and Stéphanie Delaune

In Riccardo Focardi and Andrew C. Myers, editors, Principles of Security and Trust − 4th International Conference‚ POST 2015‚ Held as Part of the European Joint Conferences on Theory and Practice of Software‚ ETAPS 2015‚ London‚ UK‚ April 11−18‚ 2015‚ Proceedings. Vol. 9036 of Lecture Notes in Computer Science. Pages 324–343. Springer. 2015.

Details about Composing Security Protocols: From Confidentiality to Privacy | BibTeX data for Composing Security Protocols: From Confidentiality to Privacy | DOI (10.1007/978-3-662-46666-7_17) | Download (pdf) of Composing Security Protocols: From Confidentiality to Privacy

Timing Attacks in Security Protocols: Symbolic Framework and Proof Techniques

Vincent Cheval and Véronique Cortier

In Riccardo Focardi and Andrew C. Myers, editors, Principles of Security and Trust − 4th International Conference‚ POST 2015‚ Held as Part of the European Joint Conferences on Theory and Practice of Software‚ ETAPS 2015‚ London‚ UK‚ April 11−18‚ 2015‚ Proceedings. Vol. 9036 of Lecture Notes in Computer Science. Pages 280–299. Springer. 2015.

Details about Timing Attacks in Security Protocols: Symbolic Framework and Proof Techniques | BibTeX data for Timing Attacks in Security Protocols: Symbolic Framework and Proof Techniques | DOI (10.1007/978-3-662-46666-7_15) | Download (pdf) of Timing Attacks in Security Protocols: Symbolic Framework and Proof Techniques

Secure Refinements of Communication Channels

Vincent Cheval‚ Véronique Cortier and Eric le Morvan

In Prahladh Harsha and G. Ramalingam, editors, 35th IARCS Annual Conference on Foundation of Software Technology and Theoretical Computer Science‚ FSTTCS 2015‚ December 16−18‚ 2015‚ Bangalore‚ India. Vol. 45 of LIPIcs. Pages 575–589. Schloss Dagstuhl − Leibniz−Zentrum für Informatik. 2015.

Details about Secure Refinements of Communication Channels | BibTeX data for Secure Refinements of Communication Channels | DOI (10.4230/LIPICS.FSTTCS.2015.575) | Download (pdf) of Secure Refinements of Communication Channels

Tests for Establishing Security Properties

Vincent Cheval‚ Stéphanie Delaune and Mark Ryan

In Matteo Maffei and Emilio Tuosto, editors, Trustworthy Global Computing − 9th International Symposium‚ TGC 2014‚ Rome‚ Italy‚ September 5−6‚ 2014. Revised Selected Papers. Vol. 8902 of Lecture Notes in Computer Science. Pages 82–96. Springer. 2014.

Details about Tests for Establishing Security Properties | BibTeX data for Tests for Establishing Security Properties | DOI (10.1007/978-3-662-45917-1_6) | Download (pdf) of Tests for Establishing Security Properties

APTE: An Algorithm for Proving Trace Equivalence

Vincent Cheval

In Erika Άbrahám and Klaus Havelund, editors, Tools and Algorithms for the Construction and Analysis of Systems − 20th International Conference‚ TACAS 2014‚ Held as Part of the European Joint Conferences on Theory and Practice of Software‚ ETAPS 2014‚ Grenoble‚ France‚ April 5−13‚ 2014. Proceedings. Vol. 8413 of Lecture Notes in Computer Science. Pages 587–592. Springer. 2014.

Details about APTE: An Algorithm for Proving Trace Equivalence | BibTeX data for APTE: An Algorithm for Proving Trace Equivalence | DOI (10.1007/978-3-642-54862-8_50) | Download (pdf) of APTE: An Algorithm for Proving Trace Equivalence

Deciding equivalence−based properties using constraint solving

Vincent Cheval‚ Véronique Cortier and Stéphanie Delaune

In Theor. Comput. Sci.. Vol. 492. Pages 1–39. 2013.

Details about Deciding equivalence−based properties using constraint solving | BibTeX data for Deciding equivalence−based properties using constraint solving | DOI (10.1016/J.TCS.2013.04.016) | Download (pdf) of Deciding equivalence−based properties using constraint solving

Proving More Observational Equivalences with ProVerif

Vincent Cheval and Bruno Blanchet

In David A. Basin and John C. Mitchell, editors, Principles of Security and Trust − Second International Conference‚ POST 2013‚ Held as Part of the European Joint Conferences on Theory and Practice of Software‚ ETAPS 2013‚ Rome‚ Italy‚ March 16−24‚ 2013. Proceedings. Vol. 7796 of Lecture Notes in Computer Science. Pages 226–246. Springer. 2013.

Details about Proving More Observational Equivalences with ProVerif | BibTeX data for Proving More Observational Equivalences with ProVerif | DOI (10.1007/978-3-642-36830-1_12) | Download (pdf) of Proving More Observational Equivalences with ProVerif

Lengths May Break Privacy − Or How to Check for Equivalences with Length

Vincent Cheval‚ Véronique Cortier and Antoine Plet

In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification − 25th International Conference‚ CAV 2013‚ Saint Petersburg‚ Russia‚ July 13−19‚ 2013. Proceedings. Vol. 8044 of Lecture Notes in Computer Science. Pages 708–723. Springer. 2013.

Details about Lengths May Break Privacy − Or How to Check for Equivalences with Length | BibTeX data for Lengths May Break Privacy − Or How to Check for Equivalences with Length | DOI (10.1007/978-3-642-39799-8_50) | Download (pdf) of Lengths May Break Privacy − Or How to Check for Equivalences with Length

Verifying Privacy−Type Properties in a Modular Way

Myrto Arapinis‚ Vincent Cheval and Stéphanie Delaune

In Stephen Chong, editor, 25th IEEE Computer Security Foundations Symposium‚ CSF 2012‚ Cambridge‚ MA‚ USA‚ June 25−27‚ 2012. Pages 95–109. IEEE Computer Society. 2012.

Details about Verifying Privacy−Type Properties in a Modular Way | BibTeX data for Verifying Privacy−Type Properties in a Modular Way | DOI (10.1109/CSF.2012.16) | Download (pdf) of Verifying Privacy−Type Properties in a Modular Way

Automatic verification of cryptographic protocols : privacy−type properties. (Vérification automatique des protocoles cryptographiques : propriétés d'équivalence)

Vincent Cheval

PhD Thesis Έcole normale supérieure de Cachan‚ France. 2012.

Details about Automatic verification of cryptographic protocols : privacy−type properties. (Vérification automatique des protocoles cryptographiques : propriétés d'équivalence) | BibTeX data for Automatic verification of cryptographic protocols : privacy−type properties. (Vérification automatique des protocoles cryptographiques : propriétés d'équivalence) | Link to Automatic verification of cryptographic protocols : privacy−type properties. (Vérification automatique des protocoles cryptographiques : propriétés d'équivalence)

Trace equivalence decision: negative tests and non−determinism

Vincent Cheval‚ Hubert Comon−Lundh and Stéphanie Delaune

In Yan Chen‚ George Danezis and Vitaly Shmatikov, editors, Proceedings of the 18th ACM Conference on Computer and Communications Security‚ CCS 2011‚ Chicago‚ Illinois‚ USA‚ October 17−21‚ 2011. Pages 321–330. ACM. 2011.

Details about Trace equivalence decision: negative tests and non−determinism | BibTeX data for Trace equivalence decision: negative tests and non−determinism | DOI (10.1145/2046707.2046744) | Download (pdf) of Trace equivalence decision: negative tests and non−determinism

Automating Security Analysis: Symbolic Equivalence of Constraint Systems

Vincent Cheval‚ Hubert Comon−Lundh and Stéphanie Delaune

In Jürgen Giesl and Reiner Hähnle, editors, Automated Reasoning‚ 5th International Joint Conference‚ IJCAR 2010‚ Edinburgh‚ UK‚ July 16−19‚ 2010. Proceedings. Vol. 6173 of Lecture Notes in Computer Science. Pages 412–426. Springer. 2010.

Details about Automating Security Analysis: Symbolic Equivalence of Constraint Systems | BibTeX data for Automating Security Analysis: Symbolic Equivalence of Constraint Systems | DOI (10.1007/978-3-642-14203-1_35) | Download (pdf) of Automating Security Analysis: Symbolic Equivalence of Constraint Systems

A decision procedure for proving observational equivalence

Vincent Cheval‚ Hubert Comon−Lundh and Stéphanie Delaune

In Michele Boreale and Steve Kremer, editors, Preliminary Proceedings of the 7th International Workshop on Security Issues in Coordination Models‚ Languages and Systems (SecCo'09). Bologna‚ Italy. October, 2009.

Details about A decision procedure for proving observational equivalence | BibTeX data for A decision procedure for proving observational equivalence | Download (pdf) of A decision procedure for proving observational equivalence