Vincent Cheval : Publications
-
[1]
Automatic verification of Finite Variant Property beyond convergent equational theories
Vincent Cheval and Caroline Fontaine
In 38th IEEE Computer Security Foundations Symposium‚ CSF 2023‚ June 16−20 2025. Santa Cruz‚ CA‚ USA. 2025.
Details about Automatic verification of Finite Variant Property beyond convergent equational theories | BibTeX data for Automatic verification of Finite Variant Property beyond convergent equational theories | Link to Automatic verification of Finite Variant Property beyond convergent equational theories
-
[2]
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
-
[3]
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
-
[4]
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
-
[5]
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
-
[6]
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
-
[7]
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
-
[8]
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
-
[9]
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!
-
[10]
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
-
[11]
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
-
[12]
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
-
[13]
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
-
[14]
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
-
[15]
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
-
[16]
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
-
[17]
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
-
[18]
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
-
[19]
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
-
[20]
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
-
[21]
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
-
[22]
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
-
[23]
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
-
[24]
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
-
[25]
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
-
[26]
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
-
[27]
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
-
[28]
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
-
[29]
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
-
[30]
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
-
[31]
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
-
[32]
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
-
[33]
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)
-
[34]
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
-
[35]
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
-
[36]
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