Publications
See also: Google Scholar, DBLP

Journals
  • [CCD17]
    V. Cheval, H. Comon-Lundh and S. Delaune. A procedure for deciding symbolic equivalence between sets of constraint systems. Information and Computation , 2017. PDF | PDF (Long version) | Bibtex | Abstract
  • [CCCK16]
    R. Chadha, V. Cheval, S. Ciobâca and S. Kremer. Automated verification of equivalence properties of cryptographic protocols. ACM Transactions on Computational Logic , 2016. Listed in ACM Computing Reviews' 21st Annual Best of Computing list of notable books and articles for 2016. PDF | Bibtex | Abstract
  • [YCR16]
    J. Yu, V. Cheval and M. Ryan. DTKI: A New Formalized PKI with Verifiable Trusted Parties. The Computer Journal , 2016. PDF | Bibtex | Abstract
  • [CCD13]
    V. Cheval, V. Cortier and S. Delaune. Deciding equivalence-based properties using constraint solving. Theoretical Computer Science , 2013. PDF | Bibtex | Abstract
Conferences
  • [CCT18]
    V. Cheval, V. Cortier and M. Turuani. A little more conversation, a little less action, a lot more satisfaction: Global states in ProVerif. In Proceedings of the 31th IEEE Computer Security Foundations Symposium (CSF'18), IEEE Computer Society Press, 2018, Accepted for publication. PDF | PDF (long version) | Bibtex | Abstract
  • [CKR18b]
    V. Cheval, S. Kremer and I. Rakotonirina. The DEEPSEC prover. In Proceedings of the 31th International Conference on Computer Aided Verification (CAV'18), Springer, 2018. PDF | Bibtex | Abstract
  • [CKR18]
    V. Cheval, S. Kremer and I. Rakotonirina. DEEPSEC: Deciding Equivalence Properties in Security Protocols - Theory and Practice. In Proceedings of the 39th IEEE Symposium on Security and Privacy (S&P'18), IEEE Computer Society Press, 2018. Distinguished paper award. PDF | PDF (long version) | Bibtex | Abstract
  • [CCW17]
    V. Cheval, V. Cortier and B. Warinschi. Secure composition of PKIs with public key protocols. In Proceedings of the 30th IEEE Computer Security Foundations Symposium (CSF'17), IEEE Computer Society Press, 2017. PDF | PDF (long version) | Bibtex | Abstract
  • [BCK17]
    K. Babel, V. Cheval and S. Kremer. On Communication Models When Verifying Equivalence Properties. In Proceedings of the 6nd International Conference on Principles of Security and Trust (POST'17), Springer Berlin Heidelberg, 2017. PDF | PDF (long version) | Bibtex | Abstract
  • [CCM15]
    V. Cheval, V. Cortier and E. Le Morvan. Secure Refinements of Communication Channels. In Proceedings of the 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015), Schloss Dagstuhl, 2015. PDF | PDF (long version) | Bibtex | Abstract
  • [CC15]
    V. Cheval and V. Cortier. Timing Attacks in Security Protocols: Symbolic Framework and Proof Techniques. In Proceedings of the 4nd International Conference on Principles of Security and Trust (POST'15), Springer Berlin Heidelberg, 2015. PDF | PDF (long version) | Bibtex | Abstract
  • [ACD15]
    M. Arapinis, V. Cheval and S. Delaune. Composing security protocols: from confidentiality to privacy. In Proceedings of the 4nd International Conference on Principles of Security and Trust (POST'15), Springer Berlin Heidelberg, 2015. PDF | PDF (long version) | Bibtex | Abstract
  • [CDR14]
    V. Cheval, S. Delaune and M. Ryan. Tests for establishing security properties. In Proceedings of the 9th Symposium on Trustworthy Global Computing (TGC'14), Springer Berlin Heidelberg, 2014. PDF | Bibtex | Abstract
  • [Che14]
    V. Cheval. APTE: an Algorithm for Proving Trace Equivalence. In Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'14), Springer, 2014. PDF | Bibtex | Abstract
  • [CCP13]
    V. Cheval, V. Cortier and A. Plet. Lengths may break privacy -- or how to check for equivalences with length. In Proceedings of the 25th International Conference on Computer Aided Verification (CAV'13), Springer, 2013. PDF | PDF (long version) | Bibtex | Abstract
  • [CB13]
    V. Cheval and B. Blanchet. Proving More Observational Equivalences with ProVerif. In Proceedings of the 2nd International Conference on Principles of Security and Trust (POST'13), Springer, 2013. PDF | PDF (long version) | Bibtex | Abstract
  • [ACD12]
    M. Arapinis, V. Cheval and S. Delaune. Verifying privacy-type properties in a modular way. In Proceedings of the 25th IEEE Computer Security Foundations Symposium (CSF'12), IEEE Computer Society Press, 2012. PDF | PDF (long version) | Bibtex | Abstract
  • [CCD11]
    V. Cheval, H. Comon-Lundh and S. Delaune. Trace Equivalence Decision: Negative Tests and Non-determinism. In Proceedings of the 18th ACM Conference on Computer and Communications Security (CCS'11), ACM Press, 2011. PDF | Bibtex | Abstract
  • [CCD10]
    V. Cheval, H. Comon-Lundh and S. Delaune. Automating security analysis: symbolic equivalence of constraint systems. In Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR'10), Springer-Verlag, 2010. PDF | Bibtex | Abstract
Theses
  • [Che12]
    V. Cheval. Automatic verification of cryptographic protocols: privacy-type properties. PhD Thesis, Laboratoire Specification et Verification, ENS Cachan, France, December 2012. PDF | Bibtex | Abstract
Other Publications