Bibliography

• 1M. Baudet, V. Cortier, S. Kremer.
  
  Computationally Sound Implementations of Equational Theories against Passive Adversaries, in: Information and Computation, April 2009, vol. 207, n^o 4, p. 496-520. [ DOI : 10.1016/j.ic.2008.12.005 ]
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCK-ic09.pdf
• 2M. Bortolozzo, M. Centenaro, R. Focardi, G. Steel.
  
  Attacking and Fixing PKCS#11 Security Tokens, in: Proceedings of the 17th ACM Conference on Computer and Communications Security (CCS'10), Chicago, Illinois, USA, ACM Press, October 2010, p. 260-269. [ DOI : 10.1145/1866307.1866337 ]
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCFS-ccs10.pdf
• 3V. Cheval, H. Comon-Lundh, S. Delaune.
  
  Trace Equivalence Decision: Negative Tests and Non-determinism, in: Proceedings of the 18th ACM Conference on Computer and Communications Security (CCS'11), Chicago, Illinois, USA, ACM Press, October 2011, To appear.
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CCD-ccs11.pdf
• 4H. Comon-Lundh, V. Cortier.
  
  Tree Automata with One Memory, Set Constraints and Cryptographic Protocols, in: Theoretical Computer Science, February 2005, vol. 331, n^o 1, p. 143-214. [ DOI : 10.1016/j.tcs.2004.09.036 ]
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ComonCortierTCS1.ps
• 5H. Comon-Lundh, V. Cortier.
  
  Computational soundness of observational equivalence, in: Proceedings of the 15th ACM Conference on Computer and Communications Security (CCS'08), Alexandria, Virginia, USA, ACM Press, October 2008, p. 109-118.
  
  http://dx.doi.org/10.1145/1455770.1455786
• 6S. Delaune, S. Kremer, M. D. Ryan.
  
  Verifying Privacy-type Properties of Electronic Voting Protocols, in: Journal of Computer Security, July 2009, vol. 17, n^o 4, p. 435-487.
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-jcs08.pdf
• 7S. Delaune, S. Kremer, G. Steel.
  
  Formal Analysis of PKCS#11 and Proprietary Extensions, in: Journal of Computer Security, 2009, To appear.
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKS-jcs09.pdf
• 8J. Goubault-Larrecq.
  
  On Noetherian Spaces, in: Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science (LICS'07), Wrocław, Poland, IEEE Computer Society Press, July 2007, p. 453-462. [ DOI : 10.1109/LICS.2007.34 ]
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JGL-lics07.pdf
• 9J. Goubault-Larrecq, F. Parrennes.
  
  Cryptographic Protocol Analysis on Real C Code, in: Proceedings of the 6th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'05), Paris, France, R. Cousot (editor), Lecture Notes in Computer Science, Springer, January 2005, vol. 3385, p. 363-379. [ DOI : 10.1007/b105073 ]
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GouPar-VMCAI2005.pdf
• 10J. Olivain, J. Goubault-Larrecq.
  
  The Orchids Intrusion Detection Tool, in: Proceedings of the 17th International Conference on Computer Aided Verification (CAV'05), Edinburgh, Scotland, UK, K. Etessami, S. Rajamani (editors), Lecture Notes in Computer Science, Springer, July 2005, vol. 3576, p. 286-290. [ DOI : 10.1007/11513988_28 ]
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/OG-cav05.pdf

Doctoral Dissertations and Habilitation Theses

• 11M. Arnaud.
  
  Formal Verification of Secured Routing Protocols, ENS Cachan, December 2011.
  
  http://www.lsv.ens-cachan.fr/~arnaud/phd/
• 12Ş. Ciobâcă.
  
  Automated Verification of Security Protocols with Applications to Electronic Voting, ENS Cachan, December 2011.
  
  http://www.lsv.ens-cachan.fr/~ciobaca/thesis
• 13S. Delaune.
  
  Verification of security protocols: from confidentiality to privacy, École Normale Supérieure de Cachan, France, March 2011, Mémoire d'habilitation.
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/hdr-SD.pdf
• 14S. Kremer.
  
  Modelling and analyzing security protocols in cryptographic process calculi, École Normale Supérieure de Cachan, France, March 2011, Mémoire d'habilitation.
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/hdr-SK.pdf
• 15G. Steel.
  
  Formal Analysis of Security APIs, École Normale Supérieure de Cachan, France, March 2011, Mémoire d'habilitation.
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/hdr-GS.pdf

Articles in International Peer-Reviewed Journal

• 16M. Backes, I. Cervesato, A. Jaggard, A. Scedrov, J.-K. Tsay.
  
  Cryptographically Sound Security Proofs for Basic and Public-Key Kerberos, in: International Journal of Information Security, 2011, vol. 10, p. 107-134, 10.1007/s10207-011-0125-6.
  
  http://dx.doi.org/10.1007/s10207-011-0125-6
• 17R. Chadha, A. P. Sistla, M. Viswanathan.
  
  Power of Randomization in Automata on Infinite Strings, in: Logical Methods in Computer Science, September 2011, vol. 7, n^o 3:22. [ DOI : 10.2168/LMCS-7(3:22)2011 ]
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CSV-lmcs11.pdf
• 18Ş. Ciobâcă, S. Delaune, S. Kremer.
  
  Computing knowledge in security protocols under convergent equational theories, in: Journal of Automated Reasoning, 2011, To appear. [ DOI : 10.1007/s10817-010-9197-7 ]
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDK-jar10.pdf
• 19V. Cortier, S. Delaune.
  
  Decidability and combination results for two notions of knowledge in security protocols, in: Journal of Automated Reasoning, 2011, To appear. [ DOI : 10.1007/s10817-010-9208-8 ]
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CD-jar10.pdf
• 20V. Cortier, S. Kremer, B. Warinschi.
  
  A Survey of Symbolic Methods in Computational Analysis of Cryptographic Systems, in: Journal of Automated Reasoning, April 2011, vol. 46, n^o 3-4, p. 225-259. [ DOI : 10.1007/s10817-010-9187-9 ]
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CKW-jar10.pdf
• 21J. Goubault-Larrecq.
  
  Musings Around the Geometry of Interaction, and Coherence, in: Theoretical Computer Science, April 2011, vol. 412, n^o 20, p. 1998-2014. [ DOI : 10.1016/j.tcs.2010.12.023 ]
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/jgl-jyg10.pdf
• 22J. Goubault-Larrecq, K. Keimel.
  
  Choquet-Kendall-Matheron Theorems for Non-Hausdorff Spaces, in: Mathematical Structures in Computer Science, June 2011, vol. 21, n^o 3, p. 511-561. [ DOI : 10.1017/S0960129510000617 ]
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GLK-mscs10.pdf
• 23F. Jacquemard, F. Klay, C. Vacher.
  
  Rigid Tree Automata, in: Information and Computation, March 2011, vol. 209, n^o 3, p. 486-512. [ DOI : 10.1016/j.ic.2010.11.015 ]
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JKV-icomp11.pdf
• 24S. Kremer, A. Mercier, R. Treinen.
  
  Reducing Equational Theories for the Decision of Static Equivalence, in: Journal of Automated Reasoning, 2011, To appear.
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KMT-jar10.pdf

International Conferences with Proceedings

• 25M. Abdalla, C. Chevalier, L. Granboulan, D. Pointcheval.
  
  Contributory Password-Authenticated Group Key Exchange with Join Capability, in: Proceedings of the Cryptographers' Track at the RSA Conference 2011 (CT-RSA'11), San Francisco, CA, USA, A. Kiayias (editor), Lecture Notes in Computer Science, Springer, February 2011, vol. 6558, p. 142-160. [ DOI : 10.1007/978-3-642-19074-2_11 ]
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACGP-rsa11.pdf
• 26M. Arnaud, V. Cortier, S. Delaune.
  
  Deciding security for protocols with recursive tests, in: Proceedings of the 23rd International Conference on Automated Deduction (CADE'11), Wrocław, Poland, N. Bjørner, V. Sofronie-Stokkermans (editors), Lecture Notes in Artificial Intelligence, Springer, July 2011, p. 49-63. [ DOI : 10.1007/978-3-642-22438-6_6 ]
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACD-cade11.pdf
• 27H. Benzina, J. Goubault-Larrecq.
  
  Some Ideas on Virtualized Systems Security, and Monitors, in: Revised Selected Papers of the 5th International Workshop on Data Privacy Management and Autonomous Spontaneous Security (DPM'10) and 3rd International Workshop on Autonomous and Spontaneous Security (SETOP'10), Athens, Greece, A. Cavalli, J. Leneutre (editors), Lecture Notes in Computer Science, Springer, September 2011, vol. 6514, p. 244-258.
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bgl-setop10.pdf
• 28R. Chadha, V. Korthikranthi, M. Viswanathan, G. Agha, Y. Kwon.
  
  Model Checking MDPs with a Unique Compact Invariant Set of Distributions, in: Proceedings of the 8th International Conference on Quantitative Evaluation of Systems (QEST'11), Aachen, Germany, IEEE Computer Society Press, September 2011, To appear.
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CKVAK-qest11.pdf
• 29R. Chadha, A. P. Sistla, M. Viswanathan.
  
  Model Checking Concurrent Programs with Nondeterminism and Randomization, in: Proceedings of the 30th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'10), Chennai, India, K. Lodaya, M. Mahajan (editors), Leibniz International Proceedings in Informatics, Leibniz-Zentrum für Informatik, December 2011, vol. 8, p. 364-375.
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CSV-fsttcs10.pdf
• 30R. Chadha, A. P. Sistla, M. Viswanathan.
  
  Probabilistic Büchi Automata with non-extremal acceptance thresholds, in: Proceedings of the 12th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'11), Austin, TX, USA, R. Jhala, D. Schmidt (editors), Lecture Notes in Computer Science, Springer, January 2011, vol. 6538, p. 103-117. [ DOI : 10.1007/978-3-642-18275-4_9ç ]
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CSV-vmcai11.pdf
• 31V. Cheval, H. Comon-Lundh, S. Delaune.
  
  Trace Equivalence Decision: Negative Tests and Non-determinism, in: Proceedings of the 18th ACM Conference on Computer and Communications Security (CCS'11), Chicago, Illinois, USA, ACM Press, October 2011, To appear.
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CCD-ccs11.pdf
• 32C. Chevalier, S. Delaune, S. Kremer.
  
  Transforming Password Protocols to Compose, in: Proceedings of the 31st Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'11), Mumbai, India, S. Chakraborty, A. Kumar (editors), Leibniz International Proceedings in Informatics, Leibniz-Zentrum für Informatik, December 2011, To appear.
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDK-fsttcs11.pdf
• 33Ş. Ciobâcă.
  
  Computing finite variants for subterm convergent rewrite systems, in: Proceedings of the 25th International Workshop on Unification (UNIF'11), Wrocław, Poland, F. Baader (editor), July 2011, To appear.
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/SC-unif11.pdf
• 34H. Comon-Lundh, V. 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 28th Annual Symposium on Theoretical Aspects of Computer Science (STACS'11), Dortmund, Germany, C. Dürr, T. Schwentick (editors), Leibniz International Proceedings in Informatics, Leibniz-Zentrum für Informatik, March 2011, vol. 9, p. 29-44. [ DOI : 10.4230/LIPIcs.STACS.2011.29 ]
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CLC-stacs11.pdf
• 35M. Dahl, S. Delaune, G. Steel.
  
  Formal Analysis of Privacy for Anonymous Location Based Services, in: Proceedings of the Workshop on Theory of Security and Applications (TOSCA'11), Saarbrücken, Germany, March-April 2011, To appear.
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DDS-tosca11.pdf
• 36S. Delaune, S. Kremer, M. D. Ryan, G. Steel.
  
  A Formal Analysis of Authentication in the TPM, in: Revised Selected Papers of the 7th International Workshop on Formal Aspects in Security and Trust (FAST'10), Pisa, Italy, P. Degano, S. Etalle, J. Guttman (editors), Lecture Notes in Computer Science, Springer, September 2011, vol. 6561, p. 111-125.
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKRS-fast10.pdf
• 37S. Delaune, S. Kremer, M. D. Ryan, G. Steel.
  
  Formal analysis of protocols based on TPM state registers, in: Proceedings of the 24th IEEE Computer Security Foundations Symposium (CSF'11), Cernay-la-Ville, France, IEEE Computer Society Press, June 2011, p. 66-82. [ DOI : 10.1109/CSF.2011.12 ]
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKRS-csf11.pdf
• 38J. Goubault-Larrecq, D. Varacca.
  
  Continuous Random Variables, in: Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science (LICS'11), Toronto, Canada, IEEE Computer Society Press, June 2011, p. 97-106. [ DOI : 10.1109/LICS.2011.23 ]
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GLV-lics2011.pdf
• 39M. Izabachène, B. Libert, D. Vergnaud.
  
  Block-wise P-Signatures and Non-Interactive Anonymous Credentials with Efficient Attributes, in: Proc. 13th IMA International Conference on Cryptography and Coding (IMACC'11), L. Chen (editor), Lecture Notes in Computer Science, Springer, 2011, vol. 7089.
• 40S. Kremer, G. Steel, B. Warinschi.
  
  Security for Key Management Interfaces, in: Proceedings of the 24th IEEE Computer Security Foundations Symposium (CSF'11), Cernay-la-Ville, France, IEEE Computer Society Press, June 2011, p. 266-280. [ DOI : 10.1109/CSF.2011.25 ]
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KSW-csf11.pdf

Conferences without Proceedings

• 41H. Benzina.
  
  Logic in Virtualized Systems, in: Proceedings of the International Conference on Computer Applications and Network Security (ICCANS'11), Republic of Maldives, May 2011.
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/benzina-iccans11.pdf
• 42O. Bouissou, É. Goubault, J. Goubault-Larrecq, S. Putot.
  
  A Generalization of P-boxes to Affine Arithmetic, and Applications to Static Analysis of Programs, in: Proceedings of the 14th GAMM-IMACS International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics (SCAN'10), Lyon, France, September 2011, To appear.

Scientific Books (or Scientific Book chapters)

• 43H. Comon-Lundh, S. Delaune, J. Millen.
  
  Constraint solving techniques and enriching the model with equational theories, in: Formal Models and Techniques for Analyzing Security Protocols, V. Cortier, S. Kremer (editors), Cryptology and Information Security Series, IOS Press, 2011, vol. 5, p. 35-61.
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDM-fmtasp11.pdf
• 44R. Focardi, F. L. Luccio, G. Steel.
  
  An Introduction to Security API Analysis, in: Foundations of Security Analysis and Design – FOSAD Tutorial Lectures (FOSAD'VI), A. Aldini, R. Gorrieri (editors), Lecture Notes in Computer Science, Springer, September 2011, vol. 6858, p. 35-65. [ DOI : 10.1007/978-3-642-23082-0_2 ]
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FLS-fosad11.pdf
• 45F. Luccio, L. Pagli, G. Steel.
  
  Mathematical and Algorithmic Foundations of the Internet, CRC Press, July 2011.
  
  http://www.amazon.co.uk/gp/product/toc/1439831386
• 46G. Steel.
  
  Formal Analysis of Security APIs, in: Encyclopedia of Cryptography and Security, H. C. A. van Tilborg, S. Jajodia (editors), Springer, 2011, p. 492-494.

Books or Proceedings Editing

• 47V. Cortier, S. Kremer (editors)
  
  Formal Models and Techniques for Analyzing Security Protocols, Cryptology and Information Security Series, IOS Press, 2011, vol. 5.
  
  http://www.iospress.nl/loadtop/load.php?isbn=9781607507130

Internal Reports

• 48R. Chadha, Ş. Ciobâcă, S. Kremer.
  
  Automated verification of equivalence properties of cryptographic protocols, October 2011.
  
  http://hal.inria.fr/inria-00632564/en/

Other Publications

• 49J. Degrieck.
  
  Réduction de graphes pour l'analyse de protocoles de routage sécurisés, Master Parisien de Recherche en Informatique, Paris, France, September 2011.
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/jd11-m2.pdf
• 50S. Delaune.
  
  Algorithms for observational equivalence, January 2011, Deliverable AVOTE 2.2, (ANR-07-SESU-002), 118 pages.
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/avote-d22.pdf
• 51S. Kremer.
  
  Results on case studies from literature, January 2011, Deliverable AVOTE 4.2, (ANR-07-SESU-002), 96 pages.
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/avote-d4-2.pdf
• 52J. Olivain, J. Goubault-Larrecq, H. Benzina, B. Gourdin, R. Ben Younès.
  
  ORCHIDS, 2011.
  
  http://www.lsv.ens-cachan.fr/Software/orchids/
• 53D. Pasailă.
  
  Verifying equivalence properties of security protocols, Master Parisien de Recherche en Informatique, Paris, France, September 2011.
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/dp11-m2.pdf

• 54M. Abadi, C. Fournet.
  
  Mobile Values, New Names, and Secure Communication, in: Proc. 28th ACM Symposium on Principles of Programming Languages (POPL'01), ACM Press, 2001, p. 104–15.
• 55M. Baudet.
  
  Deciding Security of Protocols against Off-line Guessing Attacks, in: Proceedings of the 12th ACM Conference on Computer and Communications Security (CCS'05), Alexandria, Virginia, USA, ACM Press, November 2005, p. 16-25. [ DOI : 10.1145/1102125 ]
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Baudet_CCS05revised.pdf
• 56M. Bortolozzo, M. Centenaro, R. Focardi, G. Steel.
  
  Attacking and Fixing PKCS#11 Security Tokens, in: Proceedings of the 17th ACM Conference on Computer and Communications Security (CCS'10), Chicago, Illinois, USA, ACM Press, October 2010, p. 260-269. [ DOI : 10.1145/1866307.1866337 ]
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCFS-ccs10.pdf
• 57R. Chadha, A. P. Sistla, M. Viswanathan.
  
  On the expressiveness and complexity of randomization in finite state monitors, in: Journal of the ACM, August 2009, vol. 56, n^o 5. [ DOI : 10.1145/1552285.1552287 ]
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CSV-jacm09.pdf
• 58R. Chadha, A. P. Sistla, M. Viswanathan.
  
  Model Checking Concurrent Programs with Nondeterminism and Randomization, in: Proceedings of the 30th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'10), Chennai, India, K. Lodaya, M. Mahajan (editors), Leibniz International Proceedings in Informatics, Leibniz-Zentrum für Informatik, December 2010, vol. 8, p. 364-375. [ DOI : 10.4230/LIPIcs.FSTTCS.2010.364 ]
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CSV-fsttcs10.pdf
• 59H. Comon-Lundh, S. Delaune.
  
  The finite variant property: How to get rid of some algebraic properties, in: Proceedings of the 16th International Conference on Rewriting Techniques and Applications (RTA'05), Nara, Japan, J. Giesl (editor), Lecture Notes in Computer Science, Springer, April 2005, vol. 3467, p. 294-307.
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/rta05-CD.pdf
• 60J. Goubault-Larrecq.
  
  Continuous Capacities on Continuous State Spaces, in: Proceedings of the 34th International Colloquium on Automata, Languages and Programming (ICALP'07), Wrocław, Poland, L. Arge, Ch. Cachin, T. Jurdziński, A. Tarlecki (editors), Lecture Notes in Computer Science, Springer, July 2007, vol. 4596, p. 764-776. [ DOI : 10.1007/978-3-540-73420-8_66 ]
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JGL-icalp07.pdf
• 61J. Goubault-Larrecq.
  
  Continuous Previsions, in: Proceedings of the 16th Annual EACSL Conference on Computer Science Logic (CSL'07), Lausanne, Switzerland, J. Duparc, T. A. Henzinger (editors), Lecture Notes in Computer Science, Springer, September 2007, vol. 4646, p. 542-557. [ DOI : 10.1007/978-3-540-74915-8_40 ]
  
  http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JGL-csl07.pdf