Selected Publications


Edited Books / Proceedings
  1. Véronique Cortier and Steve Kremer, editors. Formal Models and Techniques for Analyzing Security Protocols, Volume 5 of Cryptology and Information Security Series, IOS Press, 312 pages, 2011.
  2. Konstantinos Chatzikokolakis and Véronique Cortier, editors. Proceedings of the  8th International Workshop on Security Issues in Concurrency, volume 51 of Electronic Proceedings in Theoretical Computer Science, 2011. (pdf version)
  3. Véronique Cortier, Claude Kirchner, Mitsuhiro Okada, and Hideki Sakurada, editors. Formal to practical Security, volume 5458 of Lecture Notes in Computer Science, 199 pages, 2009.
    © Springer-Verlag
International Journals
  1. Mouhebeddine Berrima, Narjes Ben Rajeb, and Véronique Cortier. Deciding knowledge in security protocols under some e-voting theories. Theoretical Informatics and Applications, 2011. Online First. (research report)
  2. Véronique Cortier and Stéphanie Delaune. Decidability and combination results for two notions of knowledge in security protocols. Journal of Automated Reasoning (JAR), Online First. (draft pdf)
  3. Véronique Cortier, Steve Kremer and Bogdan Warinschi. A Survey of Symbolic Methods in Computational Analysis of Cryptographic Systems. Journal of Automated Reasoning (JAR), Volume 46, Issue 3, pages 225-259, Springer, 2011. (draft pdf)
  4. Hubert Comon-Lundh, Véronique Cortier, and Eugen Zalinescu. Deciding security properties for cryptographic protocols. Application to key cycles. ACM Transactions on Computational Logic (TOCL), ACM Digital Library, Volume 11, Issue 2, 2010.
  5. Mathieu Baudet, Véronique Cortier and Steve Kremer.  Computationally Sound Implementations of Equational Theories against Passive Adversaries. Information and Computation. Volume 207, pages 496-520, Elsevier, 2009.
  6. Véronique Cortier and Stéphanie Delaune. Safely composing security protocols. Formal Methods in System Design, Volume 34, Issue 1, 2009 (draft pdf).
  7. Véronique Cortier, Michael Rusinowitch, and Eugen Zalinescu. Relating two standard notions of secrecy. Logical Methods in Computer Science. Volume 3, Issue 3, Paper 2, July 2007.
  8. Martín Abadi and Véronique Cortier. Deciding knowledge in security protocols under equational theories. Theoretical Computer Science. Volume 367, Issues 1-2, 24 November 2006, pages 2-32. Top cited article 2005-2010 TCS paper award (draft pdf)
  9. Véronique Cortier, Xavier Goaoc, Mira Lee, and Hyeon-Suk Na. A note on maximally repeated sub-patterns of a point set. Discrete Mathematics, Volume 306, Issue 16, August 2006, pages 1965-1968 .
  10. Véronique Cortier, Stéphanie Delaune, and Pascal Lafourcade. A Survey of Algebraic Properties Used in Cryptographic Protocols. Journal of Computer Security. Volume 14, Number 1/2006, pages 1-43, IOS Press, 2006.
  11. Hubert Comon and Véronique Cortier. Tree automata with one memory, set constraints and cryptographic protocols. Theoretical Computer Science. Volume 331, Issue 1, pages 143-214, Elsevier, February 2005.
  12. Hubert Comon and Véronique Cortier. Security properties: two agents are sufficient. Science of Computer Programming, Volume 50, Issues 1-3, pages 51-71, Elsevier, March 2004.
  13. Véronique Cortier. About the decision of reachability for register machines. Theoretical Informatics and Applications, 36(4):341-358, 2002.
National Journals
  1. Véronique Cortier. Vérifier les protocoles cryptographiques. Technique et Science Informatique. Hermes Science. Volume 24, n° 1/2005, pages 115-140, 2005.
Book Chapters
  1. Cryptographie et codes secrets. Ouvrage collectif, Bibliothèque Tangente, Editions POLE, 2006.
  2. Véronique Cortier. Sécuriser les réseaux, les protocoles cryptographiques. Sur les chemins de la découverte, coordonné par Nayla Farouki. Presses Universitaires de France. 256 pages, janvier 2006.
International Conferences
  1. Véronique Cortier and Bogdan Warinschi. A Composable Computational Soundness Notion. In Proceedings of the 18th ACM Conference on Computer and Communications Security (CCS'11), Chicago, USA, October 2011. ACM Press.
  2. David Bernhard, Véronique Cortier, Olivier Pereira, Ben Smyth, and Bogdan Warinschi. Adapting Helios for provable ballot secrecy. In Proceedings of the 16th European Symposium on Research in Computer Security (ESORICS'11).
    © Springer-Verlag
  3. Véronique Cortier and Ben Smyth. Attacking and fixing Helios: An analysis of ballot secrecy. In Proceedings of the 24th IEEE Computer Security Foundations Symposium (CSF'11), Cernay, France. IEEE Computer Society Press, pages 297 - 311, 2011. (enriched Eprint version)
  4. Mathilde Arnaud, Véronique Cortier and Stéphenie Delaune.  Deciding security for protocols with recursive tests.  In Proceedings of the 23rd International Conference on Automated Deduction (CADE'11), Volume 6803 of Lecture Notes in Computer Science, pages 49-63. Springer, 2011.  (DOI)
    © Springer-Verlag
  5. Hubert Comon-Lundh and Véronique Cortier. How to prove security of communication protocols? A discussion on the soundness of formal models w.r.t. computational ones. In Proceedings of the 18th International Symposium on Theoretical Aspects of Computer Science (STACS'11), Dortmund, Germany. LIPIcs series, 2011.
  6. ŞtefanCiobâcă and Véronique Cortier.  Protocol composition for arbitrary primitives.  In Proceedings of the 23rd IEEE Computer Security Foundations Symposium (CSF'10), Edinburgh, United Kingdom. IEEE Computer Society Press, 2010. 
  7. Mathilde Arnaud, Véronique Cortier and Stéphanie Delaune.  Modeling and Verifying Ad Hoc Routing Protocols.  In Proceedings of the 23rd IEEE Computer Security Foundations Symposium (CSF'10), Edinburgh, United Kingdom. IEEE Computer Society Press, 2010.
  8. Véronique Cortier and Graham Steel. A Generic Security API for Symmetric Key Management on Cryptographic Devices. In Proceedings of the 14th European Symposium On Research In Computer Security (ESORICS'09), Saint-Malo, France, September 2009. Lecture Notes in Computer Science. Volume 5789 of Lecture Notes in Computer Science, pages 605-620. Springer, 2009.
    © Springer-Verlag
  9. Véronique Cortier and Stéphanie Delaune.  A method for proving observational equivalence. In Proceedings of the 22nd IEEE Computer Security Foundations Symposium (CSF'09), Port Jefferson, New York, USA. Pages 266-276, IEEE Computer Society Press, 2009.
  10. Mathieu Baudet, Véronique Cortier, and Stéphanie Delaune.  YAPA: A generic tool for computing intruder knowledge. In Proceedings of the 14th International Conference on Rewriting Techniques and Applications (RTA'09), Brazilia, Brazil, June 2009. Volume 5595 of Lecture Notes in Computer Science, pages 148-163. Springer, 2009.
    © Springer-Verlag
  11. Véronique Cortier. Verification of Security Protocols. In Proceedings of the 10th Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'09), Savanah, USA, January 2009. Volume 5403 of Lecture Notes in Computer Science, pages 5-13. Springer, 2009. (Invited tutorial)
    © Springer-Verlag
  12. Hubert Comon-Lundh and Véronique Cortier. Computational soundness of observational equivalence. In Proceedings of the 15th ACM Conference on Computer and Communications Security (CCS'08), Alexandria, Virginia, USA, October 2008. ACM Press.
  13. Véronique Cortier, Jérémie Delaitre, and Stéphanie Delaune. Safely Composing Security Protocols. In Proceedings of the 27th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'07), New Delhi, India, December 2007. Volume 4855 of Lecture Notes in Computer Science, pages 352-363. Springer, 2007.
    © Springer-Verlag
  14. Véronique Cortier, Bogdan Warinschi, and Eugen Zalinescu. Synthetizing secure protocols. In Proceedings of the 12th European Symposium On Research In Computer Security (ESORICS'07), Dresden, Germany, September 2007. Volume 4734 of Lecture Notes in Computer Science, pages 406-421. Springer, 2007.
    © Springer-Verlag
  15. Véronique Cortier, Ralf Küsters, and Bogdan Warinschi. A Cryptographic Model for Branching Time Security Properties -- the Case of Contract Signing Protocols. In Proceedings of the 12th European Symposium On Research In Computer Security (ESORICS'07), Dresden, Germany, September 2007. Volume 4734 of Lecture Notes in Computer Science, pages 422-437. Springer, 2007.
    © Springer-Verlag
  16. Véronique Cortier and Stéphanie Delaune.  Deciding knowledge in security protocols for monoidal equational  theories. In Proc. of the 14th Int. Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'07), Yerevan, Armenia, October 2007. Volume 4790 of Lecture Notes in Artificial Intelligence, pages 196-210. Springer, 2007.
    © Springer-Verlag
  17. Mathilde Arnaud, Véronique Cortier, and Stéphanie Delaune.  Combining algorithms for deciding knowledge in security protocols.  In Proceedings of the 6th International Symposium on Frontiers of Combining Systems (FroCoS'07), Liverpool, UK, September 2007. Volume 4720 of Lecture Notes in Artificial Intelligence, pages 103-117. Springer, 2007.
    © Springer-Verlag
  18. Véronique Cortier, Stéphanie Delaune, and Graham Steel. A Formal Theory of Key Conjuring.  In 20th IEEE Computer Security Foundations Symposium (CSF'07), Venice, Italy. IEEE Comp. Soc. Press, pages 79-93, 2007.
  19. Véronique Cortier, Gavin Keighren, and Graham Steel. Automatic Analysis of the Security of XOR-based Key Management Schemes. In Thirteenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'07), Braga, Portugal, March 2007. Volume 4424 of Lecture Notes in Computer Science, pages 538-552. Springer, 2007.
    © Springer-Verlag
  20. Véronique Cortier, Steve Kremer, Ralf Küsters, and Bogdan Warinschi. Computationally Sound Symbolic Secrecy in the Presence of Hash Functions. In Proceedings of the 26th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'06), Kolkata, India, December 2006. Volume 4337 of Lecture Notes in Computer Science, pages 176-187. Springer, 2006.
    © Springer-Verlag
  21. Véronique Cortier and Eugen Zalinescu. Deciding key cycles for security protocols. In Proc. of the 13th Int. Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'06), Phnom Penh, Cambodia, November 2006. Volume 4246 of Lecture Notes in Artificial Intelligence, pages 317-331. Springer, 2006.
    © Springer-Verlag
  22. Véronique Cortier, Michael Rusinowitch, and Eugen Zalinescu. Relating two standard notions of secrecy. In Proc. of the 20th Int. Conference Computer Science Logic (CSL'06), Szeged, Hungary, September 2006, volume 4207 of Lecture Notes in Computer Science, pages 303-318. Springer, 2006.
    © Springer-Verlag
  23. Mathieu Baudet, Véronique Cortier, and Steve Kremer. Computationally Sound Implementations of Equational Theories against Passive Adversaries, In Proc. of the 32nd International Colloquium on Automata, Languages and Programming (ICALP'05), Lisboa, Portugal, July 2005, volume 3580 of Lecture Notes in Computer Science. Springer. pages 652-663, 2005. Extended version.
    © Springer-Verlag
  24. Véronique Cortier, Michael Rusinowitch, and Eugen Zalinescu. A resolution Strategy for Verifying Cryptographic Protocols with CBC Encryption and Blind Signatures. In Proc. of the 7th ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP'05), Lisboa, Portugal, July 2005, pages 12-22, ACM press, 2005.
  25. Martín Abadi and Véronique Cortier. Deciding knowledge in security protocols under (many more) equational theories. In Proc. 18th IEEE Computer Security Foundations Workshop (CSFW'05), Aix-en-Provence, France, June 2005, pages 62-76. IEEE Comp. Soc. Press, 2005.
  26. Véronique Cortier and Bogdan Warinschi. Computationally Sound, Automated Proofs for Security Protocols. In Proc. 14th European Symposium on Programming (ESOP'05), Edinburgh, U.K., April 2005, volume 3444 of Lecture Notes in Computer Science, pages 157-171. Springer, 2005.
    © Springer-Verlag
  27. Martín Abadi and Véronique Cortier. Deciding knowledge in security protocols under equational theories. In Proc. 31st Int. Coll. Automata, Languages, and Programming (ICALP'2004), Turku, Finland, July 2004, volume 3142 of Lecture Notes in Computer Science, pages 46-58. Springer, 2004.
    © Springer-Verlag
  28. Hubert Comon-Lundh and Véronique Cortier. New decidability results for fragments of first-order logic and application to cryptographic protocols. In Proc. 14th Int. Conf. Rewriting Techniques and Applications (RTA'2003), Valencia, Spain, June 2003, volume 2706 of Lecture Notes in Computer Science, pages 148-164. Springer, 2003.
    © Springer-Verlag
  29. Hubert Comon-Lundh and Véronique Cortier. Security properties: two agents are sufficient. In Proc. 12th European Symposium on Programming (ESOP'2003), Warsaw, Poland, Apr. 2003, volume 2618 of Lecture Notes in Computer Science, pages 99-113. Springer, 2003.
    © Springer-Verlag
  30. Hubert Comon, Véronique Cortier, and John Mitchell. Tree automata with one memory, set constraints and ping-pong protocols. In Proc. 28th Int. Coll. Automata, Languages, and Programming (ICALP'2001), Crete, Greece, July 2001, volume 2076 of Lecture Notes in Computer Science, pages 682-693. Springer, 2001.
    © Springer-Verlag
  31. Véronique Cortier, Jon Millen, and Harald Rueß. Proving secrecy is easy enough. In Proc. 14th IEEE Computer Security Foundations Workshop (CSFW'01), Cape Breton, Nova Scotia, Canada, June 2001, pages 97-110. IEEE Comp. Soc. Press, 2001.
  32. Hubert Comon and Véronique Cortier. Flatness is not a weakness. In Proc. 14th Int. Conference Computer Science Logic (CSL'2000), Fischbachau, Germany, Aug. 2000, volume 1862 of Lecture Notes in Computer Science, pages 262-276. Springer, 2000.
    © Springer-Verlag
  33. Véronique Cortier, Harald Ganzinger, Florent Jacquemard, and Margus Veanes. Decidable fragments of simultaneous rigid reachability. In Proc. 26th Int. Coll. Automata, Languages, and Programming (ICALP'99), Prague, Czech Republic, July 1999, volume 1644 of Lecture Notes in Computer Science, pages 250-260. Springer, 1999. Extended version available as MPI report I-1999-2-004.
    © Springer-Verlag
Workshops
  1. Véronique Cortier, Jérémie Detrey, Pierrick Gaudry, Frédéric Sur, Emmanuel Thomé, Mathieu Turuani, and Paul Zimmermann. Ballot stuffing in a postal voting system. International Workshop on Requirements Engineering for Electronic Voting Systems (REVOTE 2011). Trento, Italy, 2011.
  2. Véronique Cortier and Bogdan Wainschi. A composable computational soundness notion (Abstract). 7th Workshop on Formal and Computational Cryptography (FCC 2011), Paris, France, June 2011.
  3. Mathilde Arnaud, Véronique Cortier and Stéphanie Delaune. Modeling and Verifying Ad Hoc Routing Protocol. 4th International Workshop on Security and Rewriting Techniques (SecReT'09), Port Jefferson, NY, USA, July 2009.
  4. Hubert Comon-Lundh and Véronique Cortier. Computational soundness of observational equivalence. 4th Workshop on Formal and Computational Cryptography (FCC 2008), Pittsburgh, United States, June 2008.
  5. Véronique Cortier and Stéphanie Delaune. Deciding knowledge in security protocols for monoidal equational theories. Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (FCS-ARSPA'07), Wrocław, Poland, July 2007. Workshop affiliated to LICS'07  and ICALP'07.
  6. Véronique Cortier, Ralf Küsters, and Bogdan Warinschi. A Cryptographic Model for Branching Time Security Properties -- the Case of Contract Signing Protocols. 3rd Workshop on Formal and Computational Cryptography (FCC 2007), Venice, Italy, July 2007.
  7. Véronique Cortier and Eugen Zalinescu. Deciding key cycles for security protocols. 3rd Workshop on Formal and Computational Cryptography (FCC 2007), Venice, Italy, July 2007.
  8. Véronique Cortier and Graham Steel. On the Decidability of a Class of XOR-based Key-management APIs. Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (FCS-ARSPA'06), Seattle, Washington, August 2006.
  9. Véronique Cortier, Heinrich Hördegen, and Bogdan Warinschi. Explicit Randomness is not Necessary when Modeling Probabilistic Encryption. Workshop on Information and Computer Security (ICS 2006), Timisoara, Romania, September 2006.
Scientific Popularization
  1. Cryptographie et codes secrets. Ouvrage collectif, Bibliothèque Tangente, Editions POLE, 2006.
  2. V. Cortier. Ces protocoles qui nous protègent. Tangente, Hors-série n°26 "Cryptographie et codes secrets", pages 42-44, juillet 2006.
  3. V. Cortier. Divers protocoles couramment utilisés en informatique. Tangente, Hors-série n°26 "Cryptographie et codes secrets", page 45, juillet 2006.
  4. V. Cortier. Protocoles cryptographiques : analyse par méthodes formelles. Techniques de l'ingénieur, dossier AF176. Bases documentaires "Mathématiques pour l'ingénieur". Avril 2006.
  5. V. Cortier. Sécuriser les réseaux, les protocoles cryptographiques. Sur les chemins de la découverte, coordonné par Nayla Farouki. Presses Universitaires de France. 256 pages, janvier 2006.
Other Publications
  1. Véronique Cortier. Analysis of cryptographic protocols: from symbolic to computational models. Habilitation à diriger des recherches. Institut National Polytechnique de Lorraine, November 2009.
  2. Véronique Cortier. On the use of formal models for proving cryptographic security notions. In the Proceedings of the Fourth Irish Conference on the mathematical Foundations of Computer Science and Information Technology (MFCSIT'06), pages 191--195, Cork, Ireland, August 2006.
  3. V. Cortier. Vérification automatique des protocoles cryptographiques. PhD Thesis, ENS de Cachan, March 2003. SPECIF Award 2003, See Stic-Hebdo n° 9. Le Monde Award 2004.
  4. Véronique Cortier, Steve Kremer, Ralf Küsters, and Bogdan Warinschi. Computationally Sound Symbolic Secrecy in the Presence of Hash Functions. Cryptology ePrint Archive: Report 2006/218, 2006.

    5. Research reports
  5. Mathilde Arnaud, Véronique Cortier, and Stéphanie Delaune. Modeling and Verifying Ad Hoc Routing Protocols. Research Report LSV-10-03, Laboratoire Spécification et Vérification, ENS Cachan, France, February 2010.
  6. Véronique Cortier, Steve Kremer, and Bogdan Warinschi. A Survey of Symbolic Methods in Computational Analysis of Cryptographic Systems. INRIA Research Report RR-6912, INRIA, 2009, 42 pages.
  7. Mouhebeddine Berrima, Narjes Ben Rajeb, and Véronique Cortier. Deciding knowledge in security protocols under some e-voting theories. INRIA Research Report RR-6903, INRIA, 2009, 29 pages.
  8. Véronique Cortier and Graham Steel. Synthesising Secure APIs. INRIA Research Report RR-6882, INRIA, 2009, 27 pages.
  9. Véronique Cortier and Stéphanie Delaune.  A method for proving observational equivalence.  Research Report LSV-09-04, Laboratoire Spécification et Vérification, ENS Cachan, France, February 2009. 21 pages.
  10. Mathieu Baudet, Véronique Cortier, and Stéphanie Delaune.  YAPA: A generic tool for computing intruder knowledge.  Research Report LSV-09-03, Laboratoire Spécification et Vérification, ENS Cachan, France, February 2009. 26 pages.
  11. Hubert Comon-Lundh and Véronique Cortier. Computational soundness of observational equivalence. INRIA Research Report RR-6508, INRIA, 2008, 39 pages.
    A new version with more examples.
  12. Véronique Cortier, Jérémie Delaitre, and Stéphanie Delaune. Safely composing security protocols. INRIA Research Report RR-6234, INRIA, 2007, 26 pages.
  13. Véronique Cortier, Bogdan Warinschi and Eugen Zalinescu. Synthesizing secure protocols. INRIA Research Report RR-6166, INRIA, 2007, 32 pages.
  14. Véronique Cortier, Stéphanie Delaune, and Graham Steel. A Formal Theory of Key Conjuring. INRIA Research Report RR-6134, INRIA, 2007, 38 pages.
  15. Mathilde Arnaud, Véronique Cortier, and Stéphanie Delaune. Combining algorithms for deciding knowledge in security protocols. INRIA Research Report RR-6118, INRIA, 2007, 27 pages. (Draft)
  16. Eugen Zalinescu, Véronique Cortier, and Michaël Rusinowitch. Relating two Standard Notions of Secrecy. INRIA Research Report RR-5908, INRIA, April 2006.
  17. Véronique Cortier, Xavier Goaoc, Mira Lee, and Hyeon-Suk Na. A note on maximally repeated sub-patterns of a point set. INRIA Research Report RR-5773, INRIA, 2005, 5 pages.
  18. Véronique Cortier and Bogdan Warinschi. Computationally Sound, Automated Proofs for Security Protocols. INRIA Research Report RR-5341, INRIA, October 2004, 23 pages.
  19. V. Cortier, S. Delaune, and P. Lafourcade. A Survey of Algebraic Properties used in Cryptographic Protocols.  Research Report LSV-04-15, Laboratoire Spécification et Vérification, ENS Cachan, France, 2004. 36 pages.
  20. V. Cortier. Observational equivalence and trace equivalence in an extension of Spi-calculus. Application to cryptographic protocols analysis. Extended version. Research Report LSV-02-3, Lab. Specification and Verification, ENS de Cachan, Cachan, France, March 2002. 33 pages.

    21. Technical reports
  21. V. Cortier, R. Küsters, and B. Warinschi. A Cryptographic Model for Branching Time Security Properties -- the Case of Contract Signing Protocols. Technical Report, 2007.
  22. V. Cortier, S. Delaune, and P. Lafourcade. A Survey of Algebraic Properties used in Cryptographic Protocols. Rapport numéro 2 du projet RNTL PROUVÉ, June 2004. 19 pages
  23. V. Cortier. A guide for Securify. Rapport numéro 13 du projet RNTL EVA, December 2003. 8 pages.
  24. V. Cortier. Outil de vérification SECURIFY. Rapport numéro 7 du projet RNTL EVA, May 2002. 6 pages.
  25. V. Cortier. Vérification de systèmes à compteurs. Mémoire de DEA, DEA de Logique de Paris VII, September 1999. 66 pages.

    26. Extended versions
  26. M. Abadi and V. Cortier. Deciding knowledge in security protocols under equational theories. Research Report INRIA, RR-5169, April 2004.
Last modified on September 14th, 2011.