Vincent Cheval : Publications
Click here to download all publications in a single bibtex file
@article{ChevalKR24,
title = "DeepSec: Deciding Equivalence Properties for Security Protocols - Improved theory and practice",
author = "Vincent Cheval and Steve Kremer and Itsaka Rakotonirina",
year = "2024",
journal = "TheoretiCS",
url = "https://doi.org/10.46298/theoretics.24.4",
volume = "3",
doi = "10.46298/THEORETICS.24.4",
}
@article{BanaCSW-popl24,
title = "On Learning Polynomial Recursive Programs",
author = "Alex Buna-Marginean and Vincent Cheval and Mahsa Shirmohammadi and James Worrell",
year = "2024",
journal = "Proc. {ACM} Program. Lang.",
number = "{POPL}",
pages = "1001--1027",
url = "https://doi.org/10.1145/3632876",
volume = "8",
doi = "10.1145/3632876",
}
@article{ChevalCK23-jcs23,
title = "Symbolic protocol verification with dice",
author = "Vincent Cheval and Rapha{\"{e}}lle Crubill{\'{e}} and Steve Kremer",
year = "2023",
journal = "J. Comput. Secur.",
number = "5",
pages = "501--538",
url = "https://www.cs.ox.ac.uk/people/vincent.cheval/publis/CCK-jcs23.pdf",
volume = "31",
doi = "10.3233/JCS-230037",
}
@inproceedings{ChevalCDHJK-Usenix23,
title = "Hash Gone Bad: Automated discovery of protocol attacks that exploit hash function weaknesses",
author = "Vincent Cheval and Cas Cremers and Alexander Dax and Lucca Hirschi and Charlie Jacomme and Steve Kremer",
year = "2023",
booktitle = "32nd {USENIX} Security Symposium, {USENIX} Security 2023, Anaheim, CA, USA, August 9-11, 2023",
editor = "Joseph A. Calandrino and Carmela Troncoso",
note = "\textbf{Distinguish Paper Award}",
pages = "5899--5916",
publisher = "{USENIX} Association",
url = "https://www.usenix.org/system/files/usenixsecurity23-cheval.pdf",
}
@inproceedings{ChevalMR-EuroSnP23,
title = "Automatic verification of transparency protocols",
author = "Vincent Cheval and Jos{\'{e}} Moreira and Mark Ryan",
year = "2023",
booktitle = "8th {IEEE} European Symposium on Security and Privacy, EuroS{\&}P 2023, Delft, Netherlands, July 3-7, 2023",
pages = "107--121",
publisher = "{IEEE}",
url = "https://www.cs.ox.ac.uk/people/vincent.cheval/publis/CMR-EuroSnP23.pdf",
doi = "10.1109/EUROSP57164.2023.00016",
}
@inproceedings{ChevalCD-csf23,
title = "Election Verifiability with ProVerif",
author = "Vincent Cheval and V{\'{e}}ronique Cortier and Alexandre Debant",
year = "2023",
booktitle = "36th {IEEE} Computer Security Foundations Symposium, {CSF} 2023, Dubrovnik, Croatia, July 10-14, 2023",
pages = "43--58",
publisher = "{IEEE}",
url = "https://www.cs.ox.ac.uk/people/vincent.cheval/publis/CCD-csf23.pdf",
doi = "10.1109/CSF57540.2023.00032",
}
@inproceedings{ChevalR23-csf23,
title = "Indistinguishability Beyond Diff-Equivalence in ProVerif",
author = "Vincent Cheval and Itsaka Rakotonirina",
year = "2023",
booktitle = "36th {IEEE} Computer Security Foundations Symposium, {CSF} 2023, Dubrovnik, Croatia, July 10-14, 2023",
note = "\textbf{Distinguished paper award}",
pages = "184--199",
publisher = "{IEEE}",
url = "https://www.cs.ox.ac.uk/people/vincent.cheval/publis/CR-csf23.pdf",
doi = "10.1109/CSF57540.2023.00036",
}
@inproceedings{ChevalJKK-usenix22,
title = "{SAPIC+:} protocol verifiers of the world, unite!",
author = "Vincent Cheval and Charlie Jacomme and Steve Kremer and Robert K{\"{u}}nnemann",
year = "2022",
booktitle = "31st {USENIX} Security Symposium, {USENIX} Security 2022, Boston, MA, USA, August 10-12, 2022",
editor = "Kevin R. B. Butler and Kurt Thomas",
pages = "3935--3952",
publisher = "{USENIX} Association",
url = "https://www.usenix.org/conference/usenixsecurity22/presentation/cheval",
}
@inproceedings{BlanchetCC-SnP22,
title = "ProVerif with Lemmas, Induction, Fast Subsumption, and Much More",
author = "Bruno Blanchet and Vincent Cheval and V{\'{e}}ronique Cortier",
year = "2022",
booktitle = "43rd {IEEE} Symposium on Security and Privacy, {SP} 2022, San Francisco, CA, USA, May 22-26, 2022",
pages = "69--86",
publisher = "{IEEE}",
url = "https://www.cs.ox.ac.uk/people/vincent.cheval/publis/BCC-snp22.pdf",
doi = "10.1109/SP46214.2022.9833653",
}
@inproceedings{ChevalCK-csf22,
title = "Symbolic protocol verification with dice: process equivalences in the presence of probabilities",
author = "Vincent Cheval and Rapha{\"{e}}lle Crubill{\'{e}} and Steve Kremer",
year = "2022",
booktitle = "35th {IEEE} Computer Security Foundations Symposium, {CSF} 2022, Haifa, Israel, August 7-10, 2022",
pages = "319--334",
publisher = "{IEEE}",
url = "https://www.cs.ox.ac.uk/people/vincent.cheval/publis/CCK-csf22.pdf",
doi = "10.1109/CSF54842.2022.9919644",
}
@inproceedings{BhargavanCW-ccs22,
title = "A Symbolic Analysis of Privacy for {TLS} 1.3 with Encrypted Client Hello",
author = "Karthikeyan Bhargavan and Vincent Cheval and Christopher A. Wood",
year = "2022",
booktitle = "Proceedings of the 2022 {ACM} {SIGSAC} Conference on Computer and Communications Security, {CCS} 2022, Los Angeles, CA, USA, November 7-11, 2022",
editor = "Heng Yin and Angelos Stavrou and Cas Cremers and Elaine Shi",
pages = "365--379",
publisher = "{ACM}",
url = "https://www.cs.ox.ac.uk/people/vincent.cheval/publis/BCW-ccs22.pdf",
doi = "10.1145/3548606.3559360",
}
@article{BabelCK-jcs20,
title = "On the semantics of communications when verifying equivalence properties",
author = "Kushal Babel and Vincent Cheval and Steve Kremer",
year = "2020",
journal = "J. Comput. Secur.",
number = "1",
pages = "71--127",
url = "https://www.cs.ox.ac.uk/people/vincent.cheval/publis/BCK-jcs20.pdf",
volume = "28",
doi = "10.3233/JCS-191366",
}
@inproceedings{DBLP:conf/birthday/ChevalKR20,
title = "The Hitchhiker's Guide to Decidability and Complexity of Equivalence Properties in Security Protocols",
author = "Vincent Cheval and Steve Kremer and Itsaka Rakotonirina",
year = "2020",
booktitle = "Logic, Language, and Security - Essays Dedicated to Andre Scedrov on the Occasion of His 65th Birthday",
editor = "Vivek Nigam and Tajana Ban Kirigin and Carolyn L. Talcott and Joshua D. Guttman and Stepan L. Kuznetsov and Boon Thau Loo and Mitsuhiro Okada",
pages = "127--145",
publisher = "Springer",
series = "Lecture Notes in Computer Science",
url = "https://www.cs.ox.ac.uk/people/vincent.cheval/publis/CKR-scedrov20.pdf",
volume = "12300",
doi = "10.1007/978-3-030-62077-6_10",
}
@inproceedings{ChevalKR19,
title = "Exploiting Symmetries When Proving Equivalence Properties for Security Protocols",
author = "Vincent Cheval and Steve Kremer and Itsaka Rakotonirina",
year = "2019",
booktitle = "Proceedings of the 2019 {ACM} {SIGSAC} Conference on Computer and Communications Security, {CCS} 2019, London, UK, November 11-15, 2019",
editor = "Lorenzo Cavallaro and Johannes Kinder and XiaoFeng Wang and Jonathan Katz",
pages = "905--922",
publisher = "{ACM}",
url = "https://www.cs.ox.ac.uk/people/vincent.cheval/publis/CKR-ccs19.pdf",
doi = "10.1145/3319535.3354260",
}
@inproceedings{ChevalKR-snp18,
title = "{DEEPSEC:} Deciding Equivalence Properties in Security Protocols Theory and Practice",
author = "Vincent Cheval and Steve Kremer and Itsaka Rakotonirina",
year = "2018",
booktitle = "2018 {IEEE} Symposium on Security and Privacy, {SP} 2018, Proceedings, 21-23 May 2018, San Francisco, California, {USA}",
note = "\textbf{Distinguished paper award}",
pages = "529--546",
publisher = "{IEEE} Computer Society",
url = "https://www.cs.ox.ac.uk/people/vincent.cheval/publis/CKR-snp18.pdf",
doi = "10.1109/SP.2018.00033",
}
@inproceedings{ChevalCT-csf18,
title = "A Little More Conversation, a Little Less Action, a Lot More Satisfaction: Global States in ProVerif",
author = "Vincent Cheval and V{\'{e}}ronique Cortier and Mathieu Turuani",
year = "2018",
booktitle = "31st {IEEE} Computer Security Foundations Symposium, {CSF} 2018, Oxford, United Kingdom, July 9-12, 2018",
pages = "344--358",
publisher = "{IEEE} Computer Society",
url = "https://www.cs.ox.ac.uk/people/vincent.cheval/publis/CCT-csf18.pdf",
doi = "10.1109/CSF.2018.00032",
}
@inproceedings{ChevalKR-cav18,
title = "The {DEEPSEC} Prover",
author = "Vincent Cheval and Steve Kremer and Itsaka Rakotonirina",
year = "2018",
booktitle = "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}",
editor = "Hana Chockler and Georg Weissenbacher",
pages = "28--36",
publisher = "Springer",
series = "Lecture Notes in Computer Science",
url = "https://www.cs.ox.ac.uk/people/vincent.cheval/publis/CKR-cav18.pdf",
volume = "10982",
doi = "10.1007/978-3-319-96142-2_4",
}
@article{ChevalCD-ic17,
title = "A procedure for deciding symbolic equivalence between sets of constraint systems",
author = "Vincent Cheval and Hubert Comon{-}Lundh and St{\'{e}}phanie Delaune",
year = "2017",
journal = "Inf. Comput.",
pages = "94--125",
url = "https://www.cs.ox.ac.uk/people/vincent.cheval/publis/CCD-ic17.pdf",
volume = "255",
doi = "10.1016/J.IC.2017.05.004",
}
@inproceedings{BabelCK-post17,
title = "On Communication Models When Verifying Equivalence Properties",
author = "Kushal Babel and Vincent Cheval and Steve Kremer",
year = "2017",
booktitle = "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",
editor = "Matteo Maffei and Mark Ryan",
pages = "141--163",
publisher = "Springer",
series = "Lecture Notes in Computer Science",
url = "https://www.cs.ox.ac.uk/people/vincent.cheval/publis/BCK-post17.pdf",
volume = "10204",
doi = "10.1007/978-3-662-54455-6_7",
}
@inproceedings{ChevalCW-csf17,
title = "Secure Composition of PKIs with Public Key Protocols",
author = "Vincent Cheval and V{\'{e}}ronique Cortier and Bogdan Warinschi",
year = "2017",
booktitle = "30th {IEEE} Computer Security Foundations Symposium, {CSF} 2017, Santa Barbara, CA, USA, August 21-25, 2017",
pages = "144--158",
publisher = "{IEEE} Computer Society",
url = "https://www.cs.ox.ac.uk/people/vincent.cheval/publis/CCW-csf17.pdf",
doi = "10.1109/CSF.2017.28",
}
@article{ChadhaCCK-tocl16,
title = "Automated Verification of Equivalence Properties of Cryptographic Protocols",
author = "Rohit Chadha and Vincent Cheval and {\c{S}}tefan Ciob{\^{a}}c{\u{a}} and Steve Kremer",
year = "2016",
journal = "{ACM} Trans. Comput. Log.",
note = "Listed in ACM Computing Reviews' 21st Annual Best of Computing list of notable books and articles for 2016",
number = "4",
pages = "23",
url = "https://www.cs.ox.ac.uk/people/vincent.cheval/publis/CCCK-tcl16.pdf",
volume = "17",
doi = "10.1145/2926715",
}
@article{YuCR-tcj16,
title = "{DTKI:} {A} New Formalized {PKI} with Verifiable Trusted Parties",
author = "Jiangshan Yu and Vincent Cheval and Mark Ryan",
year = "2016",
journal = "Comput. J.",
number = "11",
pages = "1695--1713",
url = "https://www.cs.ox.ac.uk/people/vincent.cheval/publis/YCR-tcj16.pdf",
volume = "59",
doi = "10.1093/COMJNL/BXW039",
}
@inproceedings{ArapinisCD-post15,
title = "Composing Security Protocols: From Confidentiality to Privacy",
author = "Myrto Arapinis and Vincent Cheval and St{\'{e}}phanie Delaune",
year = "2015",
booktitle = "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",
editor = "Riccardo Focardi and Andrew C. Myers",
pages = "324--343",
publisher = "Springer",
series = "Lecture Notes in Computer Science",
url = "https://www.cs.ox.ac.uk/people/vincent.cheval/publis/ACD-post15.pdf",
volume = "9036",
doi = "10.1007/978-3-662-46666-7_17",
}
@inproceedings{ChevalC-post15,
title = "Timing Attacks in Security Protocols: Symbolic Framework and Proof Techniques",
author = "Vincent Cheval and V{\'{e}}ronique Cortier",
year = "2015",
booktitle = "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",
editor = "Riccardo Focardi and Andrew C. Myers",
pages = "280--299",
publisher = "Springer",
series = "Lecture Notes in Computer Science",
url = "https://www.cs.ox.ac.uk/people/vincent.cheval/publis/CC-post15.pdf",
volume = "9036",
doi = "10.1007/978-3-662-46666-7_15",
}
@inproceedings{ChevalCM-fsttcs15,
title = "Secure Refinements of Communication Channels",
author = "Vincent Cheval and V{\'{e}}ronique Cortier and Eric le Morvan",
year = "2015",
booktitle = "35th {IARCS} Annual Conference on Foundation of Software Technology and Theoretical Computer Science, {FSTTCS} 2015, December 16-18, 2015, Bangalore, India",
editor = "Prahladh Harsha and G. Ramalingam",
pages = "575--589",
publisher = "Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik",
series = "LIPIcs",
url = "https://www.cs.ox.ac.uk/people/vincent.cheval/publis/CCM-fsttcs15.pdf",
volume = "45",
doi = "10.4230/LIPICS.FSTTCS.2015.575",
}
@inproceedings{ChevalDR-tgc14,
title = "Tests for Establishing Security Properties",
author = "Vincent Cheval and St{\'{e}}phanie Delaune and Mark Ryan",
year = "2014",
booktitle = "Trustworthy Global Computing - 9th International Symposium, {TGC} 2014, Rome, Italy, September 5-6, 2014. Revised Selected Papers",
editor = "Matteo Maffei and Emilio Tuosto",
pages = "82--96",
publisher = "Springer",
series = "Lecture Notes in Computer Science",
url = "https://www.cs.ox.ac.uk/people/vincent.cheval/publis/CDR-tgc14.pdf",
volume = "8902",
doi = "10.1007/978-3-662-45917-1_6",
}
@inproceedings{Cheval-tacas14,
title = "{APTE:} An Algorithm for Proving Trace Equivalence",
author = "Vincent Cheval",
year = "2014",
booktitle = "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",
editor = "Erika {\'{A}}brah{\'{a}}m and Klaus Havelund",
pages = "587--592",
publisher = "Springer",
series = "Lecture Notes in Computer Science",
url = "https://www.cs.ox.ac.uk/people/vincent.cheval/publis/Cheval-tacas14.pdf",
volume = "8413",
doi = "10.1007/978-3-642-54862-8_50",
}
@article{ChevalCD-tcs13,
title = "Deciding equivalence-based properties using constraint solving",
author = "Vincent Cheval and V{\'{e}}ronique Cortier and St{\'{e}}phanie Delaune",
year = "2013",
journal = "Theor. Comput. Sci.",
pages = "1--39",
url = "https://www.cs.ox.ac.uk/people/vincent.cheval/publis/CCD-tcs13.pdf",
volume = "492",
doi = "10.1016/J.TCS.2013.04.016",
}
@inproceedings{ChevalB-post13,
title = "Proving More Observational Equivalences with ProVerif",
author = "Vincent Cheval and Bruno Blanchet",
year = "2013",
booktitle = "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",
editor = "David A. Basin and John C. Mitchell",
pages = "226--246",
publisher = "Springer",
series = "Lecture Notes in Computer Science",
url = "https://www.cs.ox.ac.uk/people/vincent.cheval/publis/CB-post13.pdf",
volume = "7796",
doi = "10.1007/978-3-642-36830-1_12",
}
@inproceedings{ChevalCP-cav13,
title = "Lengths May Break Privacy - Or How to Check for Equivalences with Length",
author = "Vincent Cheval and V{\'{e}}ronique Cortier and Antoine Plet",
year = "2013",
booktitle = "Computer Aided Verification - 25th International Conference, {CAV} 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings",
editor = "Natasha Sharygina and Helmut Veith",
pages = "708--723",
publisher = "Springer",
series = "Lecture Notes in Computer Science",
url = "https://www.cs.ox.ac.uk/people/vincent.cheval/publis/CCP-cav13.pdf",
volume = "8044",
doi = "10.1007/978-3-642-39799-8_50",
}
@inproceedings{ArapinisCD-csf12,
title = "Verifying Privacy-Type Properties in a Modular Way",
author = "Myrto Arapinis and Vincent Cheval and St{\'{e}}phanie Delaune",
year = "2012",
booktitle = "25th {IEEE} Computer Security Foundations Symposium, {CSF} 2012, Cambridge, MA, USA, June 25-27, 2012",
editor = "Stephen Chong",
pages = "95--109",
publisher = "{IEEE} Computer Society",
url = "https://www.cs.ox.ac.uk/people/vincent.cheval/publis/ACD-csf12.pdf",
doi = "10.1109/CSF.2012.16",
}
@phdthesis{Cheval-phd12,
title = "Automatic verification of cryptographic protocols : privacy-type properties. (V{\'{e}}rification automatique des protocoles cryptographiques : propri{\'{e}}t{\'{e}}s d'{\'{e}}quivalence)",
author = "Vincent Cheval",
year = "2012",
school = "{\'{E}}cole normale sup{\'{e}}rieure de Cachan, France",
url = "https://tel.archives-ouvertes.fr/tel-00861389",
}
@inproceedings{ChevalCD-ccs11,
title = "Trace equivalence decision: negative tests and non-determinism",
author = "Vincent Cheval and Hubert Comon{-}Lundh and St{\'{e}}phanie Delaune",
year = "2011",
booktitle = "Proceedings of the 18th {ACM} Conference on Computer and Communications Security, {CCS} 2011, Chicago, Illinois, USA, October 17-21, 2011",
editor = "Yan Chen and George Danezis and Vitaly Shmatikov",
pages = "321--330",
publisher = "{ACM}",
url = "https://www.cs.ox.ac.uk/people/vincent.cheval/publis/CCD-ccs11.pdf",
doi = "10.1145/2046707.2046744",
}
@inproceedings{ChevalCD-ijcar10,
title = "Automating Security Analysis: Symbolic Equivalence of Constraint Systems",
author = "Vincent Cheval and Hubert Comon{-}Lundh and St{\'{e}}phanie Delaune",
year = "2010",
booktitle = "Automated Reasoning, 5th International Joint Conference, {IJCAR} 2010, Edinburgh, UK, July 16-19, 2010. Proceedings",
editor = "J{\"{u}}rgen Giesl and Reiner H{\"{a}}hnle",
pages = "412--426",
publisher = "Springer",
series = "Lecture Notes in Computer Science",
url = "https://www.cs.ox.ac.uk/people/vincent.cheval/publis/CCD-ijcar10.pdf",
volume = "6173",
doi = "10.1007/978-3-642-14203-1_35",
}
@inproceedings{CCD-secco09,
title = "A decision procedure for proving observational equivalence",
author = "Cheval, Vincent and Comon{-}Lundh, Hubert and Delaune, St{\'e}phanie",
year = "2009",
address = "Bologna, Italy",
booktitle = "{P}reliminary {P}roceedings of the 7th {I}nternational {W}orkshop on {S}ecurity {I}ssues in {C}oordination {M}odels, {L}anguages and {S}ystems ({SecCo}'09)",
editor = "Boreale, Michele and Kremer, Steve",
month = "oct",
url = "https://www.cs.ox.ac.uk/people/vincent.cheval/publis/CCD-secco09.pdf",
}