EN FR
EN FR


Bibliography

Major publications by the team in recent years
  • 1M. Baudet, V. Cortier, S. Kremer.

    Computationally Sound Implementations of Equational Theories against Passive Adversaries, in: Information and Computation, April 2009, vol. 207, no 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, no 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, no 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
Publications of the year

Doctoral Dissertations and Habilitation Theses

  • 11H. Benzina.

    Enforcing virtualized systems security, Laboratoire Spécification et Vérification, ENS Cachan, France, December 2012.
  • 12V. Cheval.

    Automatic verification of cryptographic protocols: privacy-type properties, Laboratoire Spécification et Vérification, ENS Cachan, France, December 2012.

Articles in International Peer-Reviewed Journals

International Conferences with Proceedings

  • 22M. Arapinis, V. Cheval, S. Delaune.

    Verifying privacy-type properties in a modular way, in: Proceedings of the 25th IEEE Computer Security Foundations Symposium (CSF'12), Cambridge Massachusetts, USA, IEEE Computer Society Press, June 2012, p. 95-109. [ DOI : 10.1109/CSF.2012.16 ]

    http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACD-csf12.pdf
  • 23D. Baelde, P. Courtieu, D. Gross-Amblard, Ch. Paulin-Mohring.

    Towards Provably Robust Watermarking, in: Third International Conference on Interactive Theorem Proving (ITP'12), Princeton, NJ, USA, L. Beringer, A. P. Felty (editors), Lecture Notes in Computer Science, Springer, August 2012, vol. 7406, p. 201-216. [ DOI : 10.1007/978-3-642-32347-8_14 ]

    http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/baelde12itp.pdf
  • 24D. Baelde, G. Nadathur.

    Combining Deduction Modulo and Logics of Fixed-Point Definitions, in: Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science (LICS'12), Dubrovnik, Croatia, IEEE Computer Society Press, June 2012, p. 105-114. [ DOI : 10.1109/LICS.2012.22 ]

    http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/baelde12lics.pdf
  • 25G. Bana, H. Comon-Lundh.

    Towards Unconditional Soundness: Computationally Complete Symbolic Attacker, in: Proceedings of the 1st International Conference on Principles of Security and Trust (POST'12), Tallinn, Estonia, P. Degano, J. D. Guttman (editors), Lecture Notes in Computer Science, Springer, March 2012, vol. 7215, p. 189-208. [ DOI : 10.1007/978-3-642-28641-4_11 ]

    http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BC-post12.pdf
  • 26R. Bardou, R. Focardi, Y. Kawamoto, L. Simionato, G. Steel, J.-K. Tsay.

    Efficient Padding Oracle Attacks on Cryptographic Hardware, in: Proceedings of the 32nd Annual International Cryptology Conference (CRYPTO'12), Santa Barbara, CA, USA, R. Safavi-Naini, R. Canetti (editors), Lecture Notes in Computer Science, Springer, August 2012, vol. 7417, p. 608-625. [ DOI : 10.1007/978-3-642-32009-5_36 ]

    http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFKSST-crypto12.pdf
  • 27H. Benzina.

    A Network Policy Model for Virtualized Systems, in: Proceedings of the 17th IEEE Symposium on Computers and Communications (ISCC'12), Nevşehir, Turkey, IEEE Computer Society Press, July 2012, p. 680-683. [ DOI : 10.1109/ISCC.2012.6249376 ]

    http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/benzina-iscc12.pdf
  • 28H. Benzina.

    Towards Designing Secure Virtualized Systems, in: Proceedings of the 2nd International Conference on Digital Information and Communication Technology and its Application (DICTAP'12), Bangkok, Thailand, IEEE Computer Society Press, May 2012, p. 250-255. [ DOI : 10.1109/DICTAP.2012.6215385 ]

    http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HB-dictap12.pdf
  • 29R. Chadha, Ş. Ciobâcă, S. Kremer.

    Automated verification of equivalence properties of cryptographic protocols, in: Programming Languages and Systems - Proceedings of the 22nd European Symposium on Programming (ESOP'12), Tallinn, Estonia, H. Seidl (editor), Lecture Notes in Computer Science, Springer, March 2012, vol. 7211, p. 108-127. [ DOI : 10.1007/978-3-642-28869-2_6 ]

    http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CCK-esop12.pdf
  • 30R. Chadha, P. Madhusudan, M. Viswanathan.

    Reachability under Contextual Locking, in: Proceedings of the 18th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'12), Tallinn, Estonia, C. Flanagan, B. König (editors), Lecture Notes in Computer Science, Springer, March 2012, vol. 7214, p. 437-450. [ DOI : 10.1007/978-3-642-28756-5_30 ]

    http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CMV-tacas12.pdf
  • 31H. Comon-Lundh, V. Cortier, G. Scerri.

    Security proof with dishonest keys, in: Proceedings of the 1st International Conference on Principles of Security and Trust (POST'12), Tallinn, Estonia, P. Degano, J. D. Guttman (editors), Lecture Notes in Computer Science, Springer, March 2012, vol. 7215, p. 149-168. [ DOI : 10.1007/978-3-642-28641-4_9 ]

    http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CCS-post12.pdf
  • 32V. Cortier, J. Degrieck, S. Delaune.

    Analysing routing protocols: four nodes topologies are sufficient, in: Proceedings of the 1st International Conference on Principles of Security and Trust (POST'12), Tallinn, Estonia, P. Degano, J. D. Guttman (editors), Lecture Notes in Computer Science, Springer, March 2012, vol. 7215, p. 30-50. [ DOI : 10.1007/978-3-642-28641-4_3 ]

    http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDD-post12.pdf
  • 33S. Delaune, S. Kremer, D. Pasailă.

    Security protocols, constraint systems, and group theories, in: Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR'12), Manchester, UK, B. Gramlich, D. Miller, U. Sattler (editors), Lecture Notes in Artificial Intelligence, Springer-Verlag, June 2012, vol. 7364, p. 164-178. [ DOI : 10.1007/978-3-642-31365-3_15 ]

    http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKP-ijcar12.pdf
  • 34A. Finkel, J. Goubault-Larrecq.

    The Theory of WSTS: The Case of Complete WSTS, in: Proceedings of the 33rd International Conference on Applications and Theory of Petri Nets (ICATPN'12), Hamburg, Germany, S. Haddad, L. Pomello (editors), Lecture Notes in Computer Science, Springer, June 2012, vol. 7347, p. 3-31. [ DOI : 10.1007/978-3-642-31131-4_2 ]

    http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FGL-atpn12.pdf
  • 35M. Izabachène, B. Libert.

    Divisible E-Cash in the Standard Model, in: Proceedings of the 5th International Conference on Pairing-Based Cryptography (PAIRING'12), Cologne, Germany, M. Abdalla, T. Lange (editors), Lecture Notes in Computer Science, Springer, May 2012, To appear.

    http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/IL-pairing12.pdf
  • 36R. Künnemann, G. Steel.

    YubiSecure? Formal Security Analysis Results for the Yubikey and YubiHSM, in: Preliminary Proceedings of the 8th Workshop on Security and Trust Management (STM'12), Pisa, Italy, A. Jøsang, P. Samarati (editors), September 2012.

    http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KS-stm12.pdf

Scientific Books (or Scientific Book chapters)

  • 37J. Goubault-Larrecq.

    Non-Hausdorff Topology and Domain Theory—Selected Topics in Point-Set Topology, Cambridge University Press, 2012, To appear.

Internal Reports

References in notes
  • 44M. 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.
  • 45M. Arnaud, V. Cortier, S. 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, F. Wolter (editor), Lecture Notes in Artificial Intelligence, Springer, September 2007, vol. 4720, p. 103-117. [ DOI : 10.1007/978-3-540-74621-8_7 ]

    http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACD-frocos07.pdf
  • 46M. 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
  • 47M. Baudet, V. Cortier, S. Delaune.

    YAPA: A generic tool for computing intruder knowledge, in: Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA'09), Brasília, Brazil, R. Treinen (editor), Lecture Notes in Computer Science, Springer, June-July 2009, vol. 5595, p. 148-163.

    http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCD-rta09.pdf
  • 48M. 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
  • 49Ş. Ciobâcă, S. Delaune, S. Kremer.

    Computing knowledge in security protocols under convergent equational theories, in: Proceedings of the 22nd International Conference on Automated Deduction (CADE'09), Montreal, Canada, R. Schmidt (editor), Lecture Notes in Artificial Intelligence, Springer, August 2009, p. 355-370.
  • 50V. Cortier, S. Delaune.

    Deciding Knowledge in Security Protocols for Monoidal Equational Theories, in: Proceedings of the 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'07), Yerevan, Armenia, N. Dershowitz, A. Voronkov (editors), Lecture Notes in Artificial Intelligence, Springer, October 2007, vol. 4790, p. 196-210. [ DOI : 10.1007/978-3-540-75560-9_16 ]

    http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CD-lpar07.pdf
  • 51M. 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