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]
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]
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
-
[3]
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
-
[4]
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
-
[5]
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
-
[6]
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!
-
[7]
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
-
[8]
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
-
[9]
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
-
[10]
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
-
[11]
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
-
[12]
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ȁ