Vincent Cheval : Publications

Journal papers

• [1]

  DeepSec: Deciding Equivalence Properties for Security Protocols − Improved theory and practice

  Vincent Cheval‚ Steve Kremer and Itsaka Rakotonirina

  In TheoretiCS. Vol. 3. 2024.

  Details about DeepSec: Deciding Equivalence Properties for Security Protocols − Improved theory and practice | BibTeX data for DeepSec: Deciding Equivalence Properties for Security Protocols − Improved theory and practice | DOI (10.46298/THEORETICS.24.4) | Link to DeepSec: Deciding Equivalence Properties for Security Protocols − Improved theory and practice

• [2]

  On Learning Polynomial Recursive Programs

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

  In Proc. ACM Program. Lang.. Vol. 8. No. POPL. Pages 1001–1027. 2024.

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

• [3]

  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

• [4]

  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

• [5]

  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

• [6]

  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

• [7]

  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

• [8]

  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

Conference papers

• [1]

  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

• [2]

  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

• [3]

  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

• [4]

  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

• [5]

  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!

• [6]

  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

• [7]

  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

• [8]

  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

• [9]

  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

• [10]

  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

• [11]

  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

• [12]

  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

• [13]

  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

• [14]

  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

• [15]

  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

• [16]

  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

• [17]

  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

• [18]

  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

• [19]

  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

• [20]

  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

• [21]

  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

• [22]

  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

• [23]

  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

• [24]

  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

• [25]

  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

• [26]

  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

Theses

• [1]

  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)