Publications : SECSI

[BDJ⁺21]: D. Baelde, S. Delaune, C. Jacomme, A. Koutsos, and S. Moreau. An Interactive Prover for Protocol Verification in the Computational Model. In Proceedings of the 42nd IEEE Symposium on Security and Privacy (S&P'21), online, May 2021. IEEE Press. To appear.
[ BibTex | Web page | PDF ]
[Bae21]: D. Baelde. Contributions to the Verification of Cryptographic Protocols. Mémoire d'habilitation, École Normale Supérieure Paris-Saclay, France, February 2021.
[ BibTex | Web page | PDF ]
[CJS20]: H. Comon, C. Jacomme, and G. Scerri. Oracle simulation: a technique for protocol composition with long term shared secrets. In Proceedings of the 27th ACM Conference on Computer and Communications Security (CCS'20), pages 1427--1444, Orlando, USA, November 2020. ACM Press.
doi: 10.1145/3372297.3417229.
[ BibTex | DOI ]
[BDM20]: D. Baelde, S. Delaune, and S. Moreau. A Method for Proving Unlinkability of Stateful Protocols. In Proceedings of the 33rd IEEE Computer Security Foundations Symposium (CSF'20), pages 169--183, Boston, MA, USA, July 2020. IEEE Computer Society Press.
[ BibTex | Web page ]
[JKB20]: C. Jacomme, S. Kremer, and G. Barthe. Universal equivalence and majority on probabilistic programs over finite fields. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic In Computer Science (LICS'20), pages 155--166, Saarbrucken, Germany, July 2020. IEEE Press.
[ BibTex | Web page ]
[CFLS20]: S. Carpov, C. Fontaine, D. Ligier, and R. Sirdey. Illuminating the Dark or how to recover what should not be seen in FE-based classifiers. 2020:1--35, May 2020.
doi: 10.2478/popets-2020-0015.
[ BibTex | DOI | Web page ]
[GM20]: J. Goubault-Larrecq and F. Mynard. Convergence without Points. Houston Journal of Mathematics, 46(1):227--282, 2020.
[ BibTex | PDF ]
[GMG20]: P. Gastin, A. Manuel, and R. Govind. Reversible Regular Languages: Logical and Algebraic Characterisations. Fundamenta Informaticae, 2020. To appear.
[ BibTex ]
[FG20]: A. Finkel and J. Goubault-Larrecq. Forward analysis for WSTS, part I: completions. Mathematical Structures in Computer Science, 30(7):752--832, 2020.
doi: 10.1017/S0960129520000195.
[ BibTex | DOI | Web page | PDF ]
[Gou20b]: J. Goubault-Larrecq. Some Topological Properties of Spaces of Lipschitz Continuous Maps on Quasi-Metric Spaces. Topology and its Applications, 282, 2020.
doi: 10.1016/j.topol.2020.107281.
[ BibTex | DOI | Web page ]
[BFNS20]: D. Baelde, A. P. Felty, G. Nadathur, and A. Saurin. A special issue on structural proof theory, automated reasoning and computation in celebration of Dale Miller's 60th birthday. Mathematical Structures in Computer Science, 29(8):1007--1008, 2020.
doi: 10.1017/S0960129519000136.
[ BibTex | DOI ]
[Gou20a]: J. Goubault-Larrecq. Π⁰₂ Subsets of Domain-Complete Spaces and Countably Correlated Spaces. Topology Proceedings, 58:13--22, 2020. E-published on March 24, 2020.
[ BibTex | PDF ]
[Kou19c]: A. Koutsos. Preuves symboliques de propriétés d'indistinguabilité calculatoire. Thèse de doctorat, École Normale Supérieure Paris-Saclay, France, September 2019.
[ BibTex | Web page | PDF ]
[Kou19b]: A. Koutsos. Decidability of a Sound Set of Inference Rules for Computational Indistinguishability. In Proceedings of the 32nd IEEE Computer Security Foundations Symposium (CSF'19), pages 48--61, Hoboken, NJ, USA, July 2019. IEEE Computer Society Press.
doi: 10.1109/CSF.2019.00011.
[ BibTex | DOI | PDF ]
[BGJ⁺19]: G. Barthe, B. Grégoire, C. Jacomme, S. Kremer, and P.-Y. Strub. Symbolic methods in computational cryptography proofs. In Proceedings of the 32nd IEEE Computer Security Foundations Symposium (CSF'19), pages 136--151, Hoboken, NJ, USA, July 2019. IEEE Computer Society Press.
doi: 10.1109/CSF.2019.00017.
[ BibTex | DOI | Web page | PDF ]
[BLS19]: D. Baelde, A. Lick, and S. Schmitz. Decidable XPath Fragments in the Real World. In Proceedings of the 38th Annual ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems (PODS'19), pages 285--302, Amsterdam, Netherlands, June-July 2019. ACM Press.
doi: 10.1145/3294052.3319685.
[ BibTex | DOI | Web page ]
[dBGJL19]: M. de Brecht, J. Goubault-Larrecq, X. Jia, and Z. Lyu. Domain-complete and LCS-complete Spaces. In Proceedings of the International Symposium on Domain Theory (ISDT'19), volume 345 of Electronic Notes in Theoretical Computer Science, pages 3--35, Yangzhou, China, June 2019. Elsevier Science Publishers.
doi: 10.1016/j.entcs.2019.07.014.
[ BibTex | DOI ]
[GJ19]: J. Goubault-Larrecq and X. Jia. Algebras of the Extended Probabilistic Powerdomain Monad. In Proceedings of the International Symposium on Domain Theory (ISDT'19), volume 345 of Electronic Notes in Theoretical Computer Science, pages 37--61, Yangzhou, China, June 2019. Elsevier Science Publishers.
doi: 10.1016/j.entcs.2019.07.015.
[ BibTex | DOI ]
[Kou19a]: A. Koutsos. The 5G-AKA Authentication Protocol Privacy. In Proceedings of the 4th IEEE European Symposium on Security and Privacy (EuroS&P'19), pages 464--479, Stockholm, Sweden, June 2019. IEEE Press.
doi: 10.1109/EuroSP.2019.00041.
[ BibTex | DOI | PDF ]
[Gou19c]: J. Goubault-Larrecq. A Probabilistic and Non-Deterministic Call-by-Push-Value Language. In Proceedings of the 34th Annual ACM/IEEE Symposium on Logic In Computer Science (LICS'19), pages 1--13, Vancouver, Canada, June 2019. IEEE Press.
doi: 10.1109/LICS.2019.8785809.
[ BibTex | DOI ]
[Gou19d]: J. Goubault-Larrecq. A semantics for nabla. Mathematical Structures in Computer Science, 29:1250--1274, 2019.
doi: 10.1017/S0960129518000063.
[ BibTex | DOI | Web page ]
[Gou19a]: J. Goubault-Larrecq. Fooling the Parallel or Tester with Probability 8/27. In The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy---Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday, volume 11760 of Lecture Notes in Computer Science, pages 313--328. Springer, 2019. Updated version on arXiv:1903.12653.
[ BibTex | Web page ]
[Gou19b]: J. Goubault-Larrecq. Formal Ball Monads. Topology and its Applications, 263:372--391, 2019.
doi: 10.1016/j.topol.2019.06.044.
[ BibTex | DOI | Web page ]
[HBD19]: L. Hirschi, D. Baelde, and S. Delaune. A method for unbounded verification of privacy-type properties. Journal of Computer Security, 27(3):277--342, 2019.
doi: 10.3233/JCS-171070.
[ BibTex | DOI | Web page | PDF ]
[Dal18]: A. Dallon. Verification of indistinguishability properties in cryptographic protocols -- Small attacks and efficient decision with SAT-Equiv. Thèse de doctorat, École Normale Supérieure Paris-Saclay, France, November 2018.
[ BibTex | Web page | PDF ]
[BFG⁺18]: G. Barthe, X. Fan, J. Gancher, B. Grégoire, C. Jacomme, and E. Shi. Symbolic Proofs for Lattice-Based Cryptography. In Proceedings of the 25th ACM Conference on Computer and Communications Security (CCS'18), pages 538--555, Toronto, Canada, October 2018. ACM Press.
[ BibTex | Web page | PDF ]
[BDH18]: D. Baelde, S. Delaune, and L. Hirschi. POR for Security Protocol Equivalences - Beyond Action-Determinism. In Proceedings of the 23rd European Symposium on Research in Computer Security (ESORICS'18), volume 11098 of Lecture Notes in Computer Science, pages 385--405, Barcelona, Spain, September 2018. Springer.
doi: 10.1007/978-3-319-99073-6_19.
[ BibTex | DOI | Web page ]
[CDD18]: V. Cortier, A. Dallon, and S. Delaune. Efficiently Deciding Equivalence for Standard Primitives and Phases. In Proceedings of the 23rd European Symposium on Research in Computer Security (ESORICS'18), volume 11098 of Lecture Notes in Computer Science, pages 491--511, Barcelona, Spain, September 2018. Springer.
doi: 10.1007/978-3-319-99073-6_24.
[ BibTex | DOI | Web page | PDF ]
[GL18]: J. Goubault-Larrecq and J.-P. Lachance. On the Complexity of Monitoring Orchids Signatures, and Recurrence Equations. Formal Methods in System Design, 53(1):6--32, August 2018. Special issue of RV'16.
doi: 10.1007/s10703-017-0303-x.
[ BibTex | DOI | Web page ]
[BLS18]: D. Baelde, A. Lick, and S. Schmitz. A Hypersequent Calculus with Clusters for Linear Frames. In Proceedings of the 10th Conference on Advances in Modal Logics (AiML'18), pages 36--55, Bern, Switzerland, August 2018. College Publications.
[ BibTex | Web page ]
[JK18]: C. Jacomme and S. Kremer. An extensive formal analysis of multi-factor authentication protocols. In Proceedings of the 31st IEEE Computer Security Foundations Symposium (CSF'18), pages 1--15, Oxford, UK, July 2018. IEEE Computer Society Press.
doi: 10.1109/CSF.2018.00008.
[ BibTex | DOI | Web page | PDF ]
[JKS18]: C. Jacomme, S. Kremer, and G. Scerri. Symbolic Models for Isolated Execution Environments. In Proceedings of the 2nd IEEE European Symposium on Security and Privacy (EuroS&P'17), pages 530--545, Paris, France, April 2018. IEEE Press.
doi: 10.1109/EuroSP.2017.16.
[ BibTex | DOI | Web page ]
[HGLJX18]: W. K. Ho, J. Goubault-Larrecq, A. Jung, and X. Xi. The Ho-Zhao Problem. Logical Methods in Computer Science, 14(1):1--19, January 2018.
doi: 10.23638/LMCS-14(1:7)2018.
[ BibTex | DOI | Web page | PDF ]
[BFG17]: M. Blondin, A. Finkel, and J. Goubault-Larrecq. Forward Analysis for WSTS, Part III: Karp-Miller Trees. In Proceedings of the 37th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'17), volume 93 of Leibniz International Proceedings in Informatics, pages 16:1--16:15, Kanpur, India, December 2017. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.FSTTCS.2017.16.
[ BibTex | DOI | Web page | PDF ]
[GN17]: J. Goubault-Larrecq and K. M. Ng. A Few Notes on Formal Balls. Logical Methods in Computer Science, 13(4):1--34, November 2017. Special Issue of the Domains XII Workshop.
doi: 10.23638/LMCS-13(4:18)2017.
[ BibTex | DOI | Web page | PDF ]
[DGG17]: J. Dubut, É. Goubault, and J. Goubault-Larrecq. Directed homology theories and Eilenberg-Steenrod axioms. Applied Categorical Structures, 25(5):775--807, October 2017.
doi: doi:10.1007/s10485-016-9438-y.
[ BibTex | DOI | Web page | PDF ]
[CDD17b]: V. Cortier, A. Dallon, and S. Delaune. A typing result for trace inclusion (for pair and symmetric encryption only). Research Report hal-01615265, HAL, October 2017.
[ BibTex | Web page | PDF ]
[Gou17a]: J. Goubault-Larrecq. Isomorphism theorems between models of mixed choice. Mathematical Structures in Computer Science, 27(6):1032--1067, September 2017.
doi: 10.1017/S0960129515000547.
[ BibTex | DOI | Web page | PDF ]
[Dub17]: J. Dubut. Directed homotopic and homologic theories for geometric models of true concurrency. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, September 2017.
[ BibTex | Web page | PDF ]
[BDGK17]: D. Baelde, S. Delaune, I. Gazeau, and S. Kremer. Symbolic Verification of Privacy-Type Properties for Security Protocols with XOR. In Proceedings of the 30th IEEE Computer Security Foundations Symposium (CSF'17), pages 234--248, Santa Barbara, California, USA, August 2017. IEEE Computer Society Press.
doi: 10.1109/CSF.2017.22.
[ BibTex | DOI | Web page | PDF ]
[CDD17a]: V. Cortier, A. Dallon, and S. Delaune. SAT-Equiv: An Efficient Tool for Equivalence Properties. In Proceedings of the 30th IEEE Computer Security Foundations Symposium (CSF'17), pages 481--494, Santa Barbara, California, USA, August 2017. IEEE Computer Society Press.
doi: 10.1109/CSF.2017.15.
[ BibTex | DOI | Web page | PDF ]
[CK17]: H. Comon and A. Koutsos. Formal Computational Unlinkability Proofs of RFID Protocols. In Proceedings of the 30th IEEE Computer Security Foundations Symposium (CSF'17), pages 100--114, Santa Barbara, California, USA, August 2017. IEEE Computer Society Press.
doi: 10.1109/CSF.2017.9.
[ BibTex | DOI | Web page | PDF ]
[CGKM17]: S. Calzavara, I. Grishchenko, A. Koutsos, and M. Maffei. A Sound Flow-Sensitive Heap Abstraction for the Static Analysis of Android Applications. In Proceedings of the 30th IEEE Computer Security Foundations Symposium (CSF'17), pages 22--36, Santa Barbara, California, USA, August 2017. IEEE Computer Society Press.
doi: 10.1109/CSF.2017.19.
[ BibTex | DOI | Web page | PDF ]
[Dou17a]: A. Doumane. Constructive completeness for the linear-time μ-calculus. In Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic In Computer Science (LICS'17), pages 1--12, Reykjavik, Iceland, June 2017. IEEE Press.
doi: 10.1109/LICS.2017.8005075.
[ BibTex | DOI ]
[Dou17b]: A. Doumane. On the infinitary proof theory of logics with fixed points. Thèse de doctorat, Université Paris-Diderot, Paris, France, June 2017.
[ BibTex | Web page | PDF ]
[KV17]: A. Koutsos and V. Vianu. Process-centric views of data-driven business artifacts. Journal of Computer and System Sciences, 86(1):82--107, June 2017.
doi: 10.1016/j.jcss.2016.11.012.
[ BibTex | DOI | Web page | PDF ]
[OBH17]: P. O'Hanlon, R. Borgaonkar, and L. Hirschi. Mobile subscriber WiFi privacy. In Proceedings of Mobile Security Technologies (MoST'17), held as part of the IEEE Computer Society Security and Privacy Workshops, San Jose, CA, USA, May 2017.
[ BibTex | PDF ]
[Hir17]: L. Hirschi. Automated Verification of Privacy in Security Protocols: Back and Forth Between Theory & Practice. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, April 2017.
[ BibTex | Web page | PDF ]
[Gou17b]: J. Goubault-Larrecq. A Non-Hausdorff Minimax Theorem. Minimax Theory and its Applications, 3(1):73--80, 2017.
[ BibTex ]
[BCMW17]: D. Baelde, A. Carayol, R. Matthes, and I. Walukiewicz. Preface: Special Issue of Fixed Points in Computer Science (FICS'13). Fundamenta Informaticae, 150(3-4):i--ii, 2017.
doi: 10.3233/FI-2017-1468.
[ BibTex | DOI | Web page ]
[BDH17]: D. Baelde, S. Delaune, and L. Hirschi. A Reduced Semantics for Deciding Trace Equivalence. Logical Methods in Computer Science, 13(2:8):1--48, 2017.
doi: 10.23638/LMCS-13(2:8)2017.
[ BibTex | DOI | Web page | PDF ]
[CCD17]: V. Cheval, H. Comon-Lundh, and S. Delaune. A procedure for deciding symbolic equivalence between sets of constraint systems. Information and Computation, 255:94--125, 2017.
doi: 10.1016/j.ic.2017.05.004.
[ BibTex | DOI | Web page ]
[Gou16d]: J. Goubault-Larrecq. A semantics for . Invited talk, Dale Miller Festschrift, Paris Diderot University, Paris, December 2016.
[ BibTex ]
[Jac16]: C. Jacomme. Automated applications of Cryptographic Assumptions. Rapport de Master, Master Parisien de Recherche en Informatique, Paris, France, September 2016.
[ BibTex | PDF ]
[GL16]: J. Goubault-Larrecq and J. Lachance. On the Complexity of Monitoring Orchids Signatures. In Proceedings of the 16th Conference on Runtime Verification (RV'16), volume 10012 of Lecture Notes in Computer Science, pages 169--164, Madrid, Spain, September 2016. Springer.
doi: 10.1007/978-3-319-46982-9_11.
[ BibTex | DOI ]
[DGG16b]: J. Dubut, É. Goubault, and J. Goubault-Larrecq. The Directed Homotopy Hypothesis. In Proceedings of the 25th Annual EACSL Conference on Computer Science Logic (CSL'16), volume 62 of Leibniz International Proceedings in Informatics, pages 9:1--9:16, Marseille, France, September 2016. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.CSL.2016.9.
[ BibTex | DOI | Web page | PDF ]
[DBS16]: A. Doumane, D. Baelde, and A. Saurin. Infinitary proof theory: the multiplicative additive case. In Proceedings of the 25th Annual EACSL Conference on Computer Science Logic (CSL'16), volume 62 of Leibniz International Proceedings in Informatics, pages 42:1--42:17, Marseille, France, September 2016. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.CSL.2016.42.
[ BibTex | DOI ]
[BLS16]: D. Baelde, S. Lunel, and S. Schmitz. A Sequent Calculus for a Modal Logic on Finite Data Trees. In Proceedings of the 25th Annual EACSL Conference on Computer Science Logic (CSL'16), volume 62 of Leibniz International Proceedings in Informatics, pages 32:1--32:16, Marseille, France, September 2016. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.CSL.2016.32.
[ BibTex | DOI | Web page ]
[DGG16a]: J. Dubut, É. Goubault, and J. Goubault-Larrecq. Bisimulations and unfolding in P-accessible categorical models. In Proceedings of the 27th International Conference on Concurrency Theory (CONCUR'16), volume 59 of Leibniz International Proceedings in Informatics, pages 25:1--25:14, Québec City, Canada, August 2016. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.CONCUR.2016.25.
[ BibTex | DOI | Web page | PDF ]
[Gou16a]: J. Goubault-Larrecq. A few things on Noetherian spaces. Invited talk (plenary speaker), Summer Topology Conference, Leicester, UK, August 2016.
[ BibTex ]
[Gou16b]: J. Goubault-Larrecq. An introduction to asymmetric topology and domain theory: why, what, and how. Invited talk, Galway Symposium, Leicester, UK, August 2016.
[ BibTex ]
[GS16]: J. Goubault-Larrecq and S. Schmitz. Deciding Piecewise Testable Separability for Regular Tree Languages. In Proceedings of the 43rd International Colloquium on Automata, Languages and Programming (ICALP'16), volume 55 of Leibniz International Proceedings in Informatics, pages 97:1--97:15, Rome, Italy, July 2016. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.ICALP.2016.97.
[ BibTex | DOI | Web page ]
[DBHS16]: A. Doumane, D. Baelde, L. Hirschi, and A. Saurin. Towards Completeness via Proof Search in the Linear Time μ-calculus. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic In Computer Science (LICS'16), pages 377--386, New York City, USA, July 2016. ACM Press.
doi: 10.1145/2933575.2933598.
[ BibTex | DOI | Web page | PDF ]
[DG16a]: S. Delaune and I. Gazeau. Combination issues. Deliverable VIP 4.2 (ANR-11-JS02-0006), June 2016. 5 pages.
[ BibTex | Web page | PDF ]
[DG16b]: S. Delaune and I. Gazeau. Results on the case studies. Deliverable VIP 2.2 (ANR-11-JS02-0006), June 2016. 8 pages.
[ BibTex | Web page | PDF ]
[HBD16]: L. Hirschi, D. Baelde, and S. Delaune. A method for verifying privacy-type properties: the unbounded case. In Proceedings of the 37th IEEE Symposium on Security and Privacy (S&P'16), pages 564--581, San Jose, California, USA, May 2016. IEEECSP.
doi: 10.1109/SP.2016.40.
[ BibTex | DOI | Web page | PDF ]
[GLSHHM16]: J. Goubault-Larrecq, P.-A. Sentucq, F. Hulin-Hubard, and F. Majorczyk. Etat final des travaux engagés sur Orchids. Rapport final et fourniture 4 du contrat DGA-INRIA Orchids, May 2016.
[ BibTex ]
[GLM16]: J. Goubault-Larrecq and F. Majorczyk. Génération de signatures pour le suivi de flux d'informations. Fourniture 3 du contrat DGA-INRIA Orchids, May 2016.
[ BibTex ]
[CDD16]: V. Cortier, A. Dallon, and S. Delaune. Bounding the number of agents, for equivalence too. In Proceedings of the 5th International Conference on Principles of Security and Trust (POST'16), volume 9635 of Lecture Notes in Computer Science, pages 211--232, Eindhoven, The Netherlands, April 2016. Springer.
doi: 10.1007/978-3-662-49635-0_11.
[ BibTex | DOI | Web page | PDF ]
[DH16]: S. Delaune and L. Hirschi. A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols. Journal of Logic and Algebraic Methods in Programming, 87:127--144, 2016. To appear.
doi: 10.1016/j.jlamp.2016.10.005.
[ BibTex | DOI | Web page | PDF ]
[GSSW16]: J. Goubault-Larrecq, M. Seisenberger, V. Selivanov, and A. Weiermann. Well Quasi-Orders in Computer Science (Dagstuhl Seminar 16031). Dagstuhl Reports, 6(1):69--98, January 2016.
doi: 10.4230/DagRep.6.1.69.
[ BibTex | DOI | Web page | PDF ]
[Chr16]: R. Chrétien. Analyse automatique de propriétés d'équivalence pour les protocoles cryptographiques. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, January 2016.
[ BibTex | Web page | PDF ]
[Gou16c]: J. Goubault-Larrecq. Les méthodes formelles: l'autre arme de la cybersécurité. Encart dans l'article ”S'adapter à la cyberguerre”, de Karen Elazari, Pour La Science 459, January 2016.
[ BibTex ]
[Dal15]: A. Dallon. Verification of Cryptographic Protocols : a bound on the number of agents. Rapport de Master, Master Parisien de Recherche en Informatique, Paris, France, September 2015. 38 pages.
[ BibTex | Web page | PDF ]
[CCD15c]: R. Chrétien, V. Cortier, and S. Delaune. From security protocols to pushdown automata. ACM Transactions on Computational Logic, 17(1:3), September 2015.
doi: 10.1145/2811262.
[ BibTex | DOI | Web page | PDF ]
[CCD15a]: R. Chrétien, V. Cortier, and S. Delaune. Checking trace equivalence: How to get rid of nonces? In Proceedings of the 20th European Symposium on Research in Computer Security (ESORICS'15), Lecture Notes in Computer Science, pages 230--251, Vienna, Austria, September 2015. Springer.
doi: 10.1007/978-3-319-24177-7_12.
[ BibTex | DOI | Web page | PDF ]
[BDS15]: D. Baelde, A. Doumane, and A. Saurin. Least and Greatest Fixed Points in Ludics. In Proceedings of the 24th Annual EACSL Conference on Computer Science Logic (CSL'15), volume 41 of Leibniz International Proceedings in Informatics, pages 549--566, Berlin, Germany, September 2015. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.CSL.2015.549.
[ BibTex | DOI | Web page | PDF ]
[BDH15]: D. Baelde, S. Delaune, and L. Hirschi. Partial Order Reduction for Security Protocols. In Proceedings of the 26th International Conference on Concurrency Theory (CONCUR'15), volume 42 of Leibniz International Proceedings in Informatics, pages 497--510, Madrid, Spain, September 2015. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.CONCUR.2015.497.
[ BibTex | DOI | Web page | PDF ]
[BDK15]: D. Baelde, S. Delaune, and S. Kremer. Decision procedures for equivalence based properties (part II). Deliverable VIP 3.2 (ANR-11-JS02-0006), September 2015. 9 pages.
[ BibTex | Web page | PDF ]
[DK15]: S. Delaune and S. Kremer. Composition results for equivalence-based security properties. Deliverable VIP 3.1 (ANR-11-JS02-0006), September 2015. 6 pages.
[ BibTex | Web page | PDF ]
[Gou15b]: J. Goubault-Larrecq. Formal balls. Invited talk, Domains XII workshop, Cork, Ireland, August 2015.
[ BibTex ]
[CCD15b]: R. Chrétien, V. Cortier, and S. Delaune. Decidability of trace equivalence for protocols with nonces. In Proceedings of the 28th IEEE Computer Security Foundations Symposium (CSF'15), pages 170--184, Verona, Italy, July 2015. IEEE Computer Society Press.
doi: 10.1109/CSF.2015.19.
[ BibTex | DOI | Web page | PDF ]
[DGG15]: J. Dubut, É. Goubault, and J. Goubault-Larrecq. Natural Homology. In Proceedings of the 42nd International Colloquium on Automata, Languages and Programming (ICALP'15) -- Part II, volume 9135 of Lecture Notes in Computer Science, pages 171--183, Kyoto, Japan, July 2015. Springer.
doi: 10.1007/978-3-662-47666-6_14.
[ BibTex | DOI | Web page | PDF ]
[GLSM15]: J. Goubault-Larrecq, P.-A. Sentucq, and F. Majorczyk. Etat d'avancement intermédiaire des travaux engagés sur OrchIDS. Rapport intermédiaire du contrat DGA-INRIA Orchids, May 2015.
[ BibTex ]
[ACD15]: M. Arapinis, V. Cheval, and S. Delaune. Composing security protocols: from confidentiality to privacy. In Proceedings of the 4th International Conference on Principles of Security and Trust (POST'15), volume 9036 of Lecture Notes in Computer Science, pages 324--343, London, UK, April 2015. Springer.
doi: 10.1007/978-3-662-46666-7_17.
[ BibTex | DOI | Web page | PDF ]
[Gou15c]: J. Goubault-Larrecq. Full Abstraction for Non-Deterministic and Probabilistic Extensions of PCF I: the Angelic Cases. Journal of Logic and Algebraic Methods in Programming, 84(1):155--184, January 2015.
doi: 10.1016/j.jlamp.2014.09.003.
[ BibTex | DOI | Web page | PDF ]
[Gou15a]: J. Goubault-Larrecq. A short proof of the Schröder-Simpson theorem. Mathematical Structures in Computer Science, 25(1):1--5, January 2015.
doi: 10.1017/S0960129513000467.
[ BibTex | DOI | Web page | PDF ]
[Sce15]: G. Scerri. Proofs of security protocols revisited. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, January 2015.
[ BibTex | Web page | PDF ]
[CDR14]: V. Cheval, S. Delaune, and M. D. Ryan. Tests for establishing security properties. In Revised Selected Papers of the 9th Symposium on Trustworthy Global Computing (TGC'14), volume 8902 of Lecture Notes in Computer Science, pages 82--96, Rome, Italy, December 2014. Springer.
doi: 10.1007/978-3-662-45917-1_6.
[ BibTex | DOI | Web page | PDF ]
[Gou14a]: J. Goubault-Larrecq. Détection d'intrusions avec OrchIDS. Matinale de l'innovation Logiciels Libres et Sécurité, Paris, France, December 2014.
[ BibTex ]
[BC14]: G. Bana and H. Comon-Lundh. A Computationally Complete Symbolic Attacker for Equivalence Properties. In Proceedings of the 21st ACM Conference on Computer and Communications Security (CCS'14), pages 609--620, Scottsdale, Arizona, USA, November 2014. ACM Press.
doi: 10.1145/2660267.2660276.
[ BibTex | DOI | Web page | PDF ]
[ACD14]: M. Arnaud, V. Cortier, and S. Delaune. Modeling and Verifying Ad Hoc Routing Protocols. Information and Computation, 238:30--67, November 2014.
doi: 10.1016/j.ic.2014.07.004.
[ BibTex | DOI | Web page | PDF ]
[BCD14]: S. Bursuc, H. Comon-Lundh, and S. Delaune. Deducibility constraints and blind signatures. Information and Computation, 238:106--127, November 2014.
doi: 10.1016/j.ic.2014.07.006.
[ BibTex | DOI | Web page | PDF ]
[AFG14]: S. Abiteboul, L. Fribourg, and J. Goubault-Larrecq. Gérard Berry : un informaticien médaille d'or du CNRS 2014. 1024 -- Bulletin de la société informatique de France, 4:139--142, October 2014.
[ BibTex | Web page | PDF ]
[Lef14]: E. Lefaucheux. Détection de fautes dans les systèmes probabilistes. Rapport de Master, Master Parisien de Recherche en Informatique, Paris, France, September 2014. 35 pages.
[ BibTex | Web page | PDF ]
[Dub14]: J. Dubut. Homologie dirigée. Rapport de Master, Master Parisien de Recherche en Informatique, Paris, France, September 2014. 35 pages.
[ BibTex | Web page | PDF ]
[CD14]: R. Chrétien and S. Delaune. Le bitcoin, une monnaie 100% numérique. Interstices, September 2014.
[ BibTex | Web page | PDF ]
[CCD14]: R. Chrétien, V. Cortier, and S. Delaune. Typing messages for free in security protocols: the case of equivalence properties. In Proceedings of the 25th International Conference on Concurrency Theory (CONCUR'14), volume 8704 of Lecture Notes in Computer Science, pages 372--386, Rome, Italy, September 2014. Springer.
doi: 10.1007/978-3-662-44584-6_26.
[ BibTex | DOI | Web page | PDF ]
[Gou14c]: J. Goubault-Larrecq. Noetherian spaces. Invited talk, Continuity, Computability, Constructivity workshop (CCC), Ljubljana, Slovenia, September 2014.
[ BibTex ]
[Gou14d]: J. Goubault-Larrecq. OrchIDS: on the value of rigor in intrusion detection. CPS Summer School, Grenoble, France, July 2014.
[ BibTex ]
[GJ14]: J. Goubault-Larrecq and A. Jung. QRB, QFS, and the Probabilistic Powerdomain. In Proceedings of the 30th Conference on Mathematical Foundations of Programming Semantics (MFPS'14), volume 308 of Electronic Notes in Theoretical Computer Science, pages 167--182, Ithaca, New York, USA, June 2014. Elsevier Science Publishers.
doi: 10.1016/j.entcs.2014.10.010.
[ BibTex | DOI | Web page | PDF ]
[ADK14]: M. Arapinis, S. Delaune, and S. Kremer. Dynamic Tags for Security Protocols. Logical Methods in Computer Science, 10(2:11), June 2014.
doi: 10.2168/LMCS-10(2:11)2014.
[ BibTex | DOI | Web page | PDF ]
[Gou14b]: J. Goubault-Larrecq. Exponentiable streams and prestreams. Applied Categorical Structures, 22(3):515--549, June 2014. Errata 1: http://www.lsv.fr/Publis/PAPERS/PDF/GL-acs13-erratum.pdf; Errata 2: http://www.lsv.fr/Publis/PAPERS/PDF/GL-acs13-erratum2.pdf.
doi: 10.1007/s10485-013-9315-x.
[ BibTex | DOI | Web page | PDF ]
[GLSM14b]: J. Goubault-Larrecq, P.-A. Sentucq, and F. Majorczyk. Techniques et méthodes de génération de signatures pour la détection d'intrusions. Fourniture 2 du contrat DGA-INRIA Orchids, May 2014.
[ BibTex ]
[GLSM14a]: J. Goubault-Larrecq, P.-A. Sentucq, and F. Majorczyk. Politiques de sécurité système. Fourniture 1 du contrat DGA-INRIA Orchids, May 2014.
[ BibTex ]
[BDH14]: D. Baelde, S. Delaune, and L. Hirschi. A reduced semantics for deciding trace equivalence using constraint systems. In Proceedings of the 3rd International Conference on Principles of Security and Trust (POST'14), volume 8414 of Lecture Notes in Computer Science, pages 1--21, Grenoble, France, April 2014. Springer.
doi: 10.1007/978-3-642-54792-8_1.
[ BibTex | DOI | Web page | PDF ]
[ABG⁺14]: A. Adjé, O. Bouissou, J. Goubault-Larrecq, É. Goubault, and S. Putot. Static Analysis of Programs with Imprecise Probabilistic Inputs. In Revised Selected Papers of the 5th IFIP TC2/WG2.3 Conference Verified Software---Theories, Tools, and Experiments (VSTTE'13), volume 8164 of Lecture Notes in Computer Science, pages 22--47, Atherton, California, USA, 2014. Springer.
doi: 10.1007/978-3-642-54108-7.
[ BibTex | DOI | Web page | PDF ]
[GS14]: J. Goubault-Larrecq and R. Segala. Random Measurable Selections. In Horizons of the Mind. A Tribute to Prakash Panangaden, volume 8464 of Lecture Notes in Computer Science, pages 343--362. Springer, 2014.
doi: 10.1007/978-3-319-06880-0_18.
[ BibTex | DOI | Web page | PDF ]
[BCG⁺14]: D. Baelde, K. Chaudhuri, A. Gacek, D. Miller, G. Nadathur, A. Tiu, and Y. Wang. Abella: A System for Reasoning about Relational Specifications. Journal of Formalized Reasoning, 7(2):1--89, 2014.
doi: 10.6092/issn.1972-5787/4650.
[ BibTex | DOI | Web page | PDF ]
[CDKR13]: C. Chevalier, S. Delaune, S. Kremer, and M. D. Ryan. Composition of Password-based Protocols. Formal Methods in System Design, 43(3):369--413, December 2013.
doi: 10.1007/s10703-013-0184-6.
[ BibTex | DOI | Web page | PDF ]
[CD13b]: R. Chrétien and S. Delaune. La protection des informations sensibles. Pour La Science, 433:70--77, November 2013.
[ BibTex | Web page ]
[GO13]: J. Goubault-Larrecq and J. Olivain. On the Efficiency of Mathematics in Intrusion Detection: The NetEntropy Case. In Revised Selected Papers of the 6th International Symposium on Foundations and Practice of Security (FPS'13), volume 8352 of Lecture Notes in Computer Science, pages 3--16, La Rochelle, France, October 2013. Springer.
doi: 10.1007/978-3-319-05302-8_1.
[ BibTex | DOI | Web page | PDF ]
[Hir13a]: L. Hirschi. Réduction d'entrelacements pour l'équivalence de traces. Research Report LSV-13-13, Laboratoire Spécification et Vérification, ENS Cachan, France, September 2013. 22 pages.
[ BibTex | Web page | PDF ]
[KKS13]: S. Kremer, R. Künnemann, and G. Steel. Universally Composable Key-Management. In Proceedings of the 18th European Symposium on Research in Computer Security (ESORICS'13), volume 8134 of Lecture Notes in Computer Science, pages 327--344, Egham, U.K., September 2013. Springer.
doi: 10.1007/978-3-642-40203-6_19.
[ BibTex | DOI | Web page | PDF ]
[Gou13a]: J. Goubault-Larrecq. A Constructive Proof of the Topological Kruskal Theorem. In Proceedings of the 38th International Symposium on Mathematical Foundations of Computer Science (MFCS'13), volume 8087 of Lecture Notes in Computer Science, pages 22--41, Klosterneuburg, Austria, August 2013. Springer.
doi: 10.1007/978-3-642-40313-2_3.
[ BibTex | DOI | Web page | PDF ]
[Hir13b]: L. Hirschi. Reduction of interleavings for trace equivalence checking of security protocols. Rapport de Master, Master Parisien de Recherche en Informatique, Paris, France, August 2013.
[ BibTex ]
[CCD13b]: R. Chrétien, V. Cortier, and S. Delaune. From security protocols to pushdown automata. In Proceedings of the 40th International Colloquium on Automata, Languages and Programming (ICALP'13) -- Part II, volume 7966 of Lecture Notes in Computer Science, pages 137--149, Riga, Latvia, July 2013. Springer.
doi: 10.1007/978-3-642-39212-2_15.
[ BibTex | DOI | Web page | PDF ]
[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), volume 8044 of Lecture Notes in Computer Science, pages 708--723, Saint Petersburg, Russia, July 2013. Springer.
doi: 10.1007/978-3-642-39799-8_50.
[ BibTex | DOI | Web page | PDF ]
[Gou13b]: J. Goubault-Larrecq. A few pearls in the theory of quasi-metric spaces. Invited talk (semi-plenary speaker), Summer Topology Conference, North Bay, Ontario, CA, July 2013.
[ BibTex ]
[Gou13e]: J. Goubault-Larrecq. A short proof of the Schröder-Simpson theorem. Invited talk, Workshop on Asymmetric Topology, Summer Topology Conference, North Bay, Ontario, CA, July 2013.
[ BibTex ]
[CCD13a]: V. Cheval, V. Cortier, and S. Delaune. Deciding equivalence-based properties using constraint solving. Theoretical Computer Science, 492:1--39, June 2013.
doi: 10.1016/j.tcs.2013.04.016.
[ BibTex | DOI | Web page | PDF ]
[CCS13]: H. Comon-Lundh, V. Cortier, and G. Scerri. Tractable inference systems: an extension with a deducibility predicate. In Proceedings of the 24th International Conference on Automated Deduction (CADE'13), volume 7898 of Lecture Notes in Artificial Intelligence, pages 91--108, Lake Placid, New York, USA, June 2013. Springer.
doi: 10.1007/978-3-642-38574-2_6.
[ BibTex | DOI | Web page | PDF ]
[Gou13d]: J. Goubault-Larrecq. OrchIDS, ou : de l'importance de la sémantique. Séminaire DGA Innosciences. DGA, Bagneux, June 2013.
[ BibTex ]
[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), volume 7796 of Lecture Notes in Computer Science, pages 226--246, Rome, Italy, March 2013. Springer.
doi: 10.1007/978-3-642-36830-1_12.
[ BibTex | DOI | Web page | PDF ]
[CD13a]: R. Chrétien and S. Delaune. Formal analysis of privacy for routing protocols in mobile ad hoc networks. In Proceedings of the 2nd International Conference on Principles of Security and Trust (POST'13), volume 7796 of Lecture Notes in Computer Science, pages 1--20, Rome, Italy, March 2013. Springer.
doi: 10.1007/978-3-642-36830-1_1.
[ BibTex | DOI | Web page | PDF ]
[Gou13c]: J. Goubault-Larrecq. Non-Hausdorff Topology and Domain Theory---Selected Topics in Point-Set Topology, volume 22 of New Mathematical Monographs. Cambridge University Press, March 2013.
[ BibTex | Web page ]
[BCD13]: M. Baudet, V. Cortier, and S. Delaune. YAPA: A generic tool for computing intruder knowledge. ACM Transactions on Computational Logic, 14(1:4), February 2013.
doi: 10.1145/2422085.2422089.
[ BibTex | DOI | Web page | PDF ]
[GJ13]: J. Goubault-Larrecq and J.-P. Jouannaud. The Blossom of Finite Semantic Trees. In Programming Logics -- Essays in Memory of Harald Ganzinger, volume 7797 of Lecture Notes in Computer Science, pages 90--122. Springer, January 2013.
[ BibTex | Web page | PDF ]
[CU12]: R. Chadha and M. Ummels. The complexity of quantitative information flow in recursive programs. In Proceedings of the 32nd Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'12), volume 18 of Leibniz International Proceedings in Informatics, pages 534--545, Hyderabad, India, December 2012. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.FSTTCS.2012.534.
[ BibTex | DOI | Web page | PDF ]
[Ben12b]: H. Benzina. Enforcing Virtualized Systems Security. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, December 2012.
[ BibTex | Web page | PDF ]
[Che12]: V. Cheval. Automatic verification of cryptographic protocols: privacy-type properties. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, December 2012.
[ BibTex | Web page | PDF ]
[AG12]: A. Adjé and J. Goubault-Larrecq. Concrete Semantics of Programs with Non-Deterministic and Random Inputs. Research Report cs.LO/1210.2605, Computing Research Repository, October 2012. 19 pages.
[ BibTex | Web page | PDF ]
[AGL12]: A. Adjé and J. Goubault-Larrecq. Concrete semantics of programs with non-deterministic and random inputs. Fourniture du projet ANR CPP (Confidence, Proofs, and Probabilities), WP 2, version 1, October 2012.
[ BibTex | Web page ]
[FG12]: A. Finkel and J. Goubault-Larrecq. Forward Analysis for WSTS, Part II: Complete WSTS. Logical Methods in Computer Science, 8(3:28), September 2012.
doi: 10.2168/LMCS-8(3:28)2012.
[ BibTex | DOI | Web page | PDF ]
[Chr12]: R. Chrétien. Trace equivalence of protocols for an unbounded number of sessions. Rapport de Master, Master Parisien de Recherche en Informatique, Paris, France, September 2012. 30 pages.
[ BibTex | Web page | PDF ]
[KS12]: R. Künnemann and G. Steel. YubiSecure? Formal Security Analysis Results for the Yubikey and YubiHSM. In Revised Selected Papers of the 8th Workshop on Security and Trust Management (STM'12), volume 7783 of Lecture Notes in Computer Science, pages 257--272, Pisa, Italy, September 2012. Springer.
doi: 10.1007/978-3-642-38004-4_17.
[ BibTex | DOI | Web page | PDF ]
[BFK⁺12]: R. Bardou, R. Focardi, Y. Kawamoto, L. Simionato, G. Steel, and J.-K. Tsay. Efficient Padding Oracle Attacks on Cryptographic Hardware. In Proceedings of the 32nd Annual International Cryptology Conference (CRYPTO'12), volume 7417 of Lecture Notes in Computer Science, pages 608--625, Santa Barbara, California, USA, August 2012. Springer.
doi: 10.1007/978-3-642-32009-5_36.
[ BibTex | DOI | Web page | PDF ]
[Ben12a]: H. Benzina. A Network Policy Model for Virtualized Systems. In Proceedings of the 17th IEEE Symposium on Computers and Communications (ISCC'12), pages 680--683, Nevsehir, Turkey, July 2012. IEEE Computer Society Press.
doi: 10.1109/ISCC.2012.6249376.
[ BibTex | DOI | Web page | PDF ]
[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), pages 95--109, Cambridge Massachusetts, USA, June 2012. IEEE Computer Society Press.
doi: 10.1109/CSF.2012.16.
[ BibTex | DOI | Web page | PDF ]
[DKP12]: S. Delaune, S. Kremer, and D. Pasailă. Security protocols, constraint systems, and group theories. In Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR'12), volume 7364 of Lecture Notes in Artificial Intelligence, pages 164--178, Manchester, UK, June 2012. Springer-Verlag.
doi: 10.1007/978-3-642-31365-3_15.
[ BibTex | DOI | Web page | PDF ]
[IL12]: M. Izabachène and B. Libert. Divisible E-Cash in the Standard Model. In Proceedings of the 5th International Conference on Pairing-Based Cryptography (PAIRING'12), volume 7708 of Lecture Notes in Computer Science, pages 314--332, Cologne, Germany, May 2012. Springer.
doi: 10.1007/978-3-642-36334-4_20.
[ BibTex | DOI | Web page | PDF ]
[Ben12c]: H. Benzina. Towards Designing Secure Virtualized Systems. In Proceedings of the 2nd International Conference on Digital Information and Communication Technology and its Application (DICTAP'12), pages 250--255, Bangkok, Thailand, May 2012. IEEE Computer Society Press.
doi: 10.1109/DICTAP.2012.6215385.
[ BibTex | DOI | Web page | PDF ]
[CD12a]: H. Comon-Lundh and S. Delaune. Formal Security Proofs. In Software Safety and Security, volume 33 of NATO Science for Peace and Security Series -- D: Information and Communication Security, pages 26--63. IOS Press, May 2012.
[ BibTex | Web page | PDF ]
[CD12b]: V. Cortier and S. Delaune. Decidability and combination results for two notions of knowledge in security protocols. Journal of Automated Reasoning, 48(4):441--487, April 2012.
doi: 10.1007/s10817-010-9208-8.
[ BibTex | DOI | Web page | PDF ]
[CHKS12]: H. Comon-Lundh, M. Hagiya, Y. Kawamoto, and H. Sakurada. Computational Soundness of Indistinguishability Properties without Computable Parsing. In Proceedings of the 8th International Conference on Information Security Practice and Experience (ISPEC'12), volume 7232 of Lecture Notes in Computer Science, pages 63--79, Hangzhou, China, April 2012. Springer.
doi: 10.1007/978-3-642-29101-2_5.
[ BibTex | DOI | Web page | PDF ]
[BGGP12]: O. Bouissou, É. Goubault, J. Goubault-Larrecq, and S. Putot. A Generalization of P-boxes to Affine Arithmetic, and Applications to Static Analysis of Programs. Computing, 94(2-4):189--201, March 2012.
doi: 10.1007/s00607-011-0182-8.
[ BibTex | DOI | Web page | PDF ]
[BC12]: G. Bana and 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), volume 7215 of Lecture Notes in Computer Science, pages 189--208, Tallinn, Estonia, March 2012. Springer.
doi: 10.1007/978-3-642-28641-4_11.
[ BibTex | DOI | Web page | PDF ]
[CCS12]: H. Comon-Lundh, V. Cortier, and G. Scerri. Security proof with dishonest keys. In Proceedings of the 1st International Conference on Principles of Security and Trust (POST'12), volume 7215 of Lecture Notes in Computer Science, pages 149--168, Tallinn, Estonia, March 2012. Springer.
doi: 10.1007/978-3-642-28641-4_9.
[ BibTex | DOI | Web page | PDF ]
[CDD12]: V. Cortier, J. Degrieck, and 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), volume 7215 of Lecture Notes in Computer Science, pages 30--50, Tallinn, Estonia, March 2012. Springer.
doi: 10.1007/978-3-642-28641-4_3.
[ BibTex | DOI | Web page | PDF ]
[CMV12]: R. Chadha, P. Madhusudan, and 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), volume 7214 of Lecture Notes in Computer Science, pages 437--450, Tallinn, Estonia, March 2012. Springer.
doi: 10.1007/978-3-642-28756-5_30.
[ BibTex | DOI | Web page | PDF ]
[CCK12]: R. Chadha, S. Ciobâcă, and 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), volume 7211 of Lecture Notes in Computer Science, pages 108--127, Tallinn, Estonia, March 2012. Springer.
doi: 10.1007/978-3-642-28869-2_6.
[ BibTex | DOI | Web page | PDF ]
[KMT12]: S. Kremer, A. Mercier, and R. Treinen. Reducing Equational Theories for the Decision of Static Equivalence. Journal of Automated Reasoning, 2(48):197--217, February 2012.
doi: 10.1007/s10817-010-9203-0.
[ BibTex | DOI | Web page | PDF ]
[CDK12]: S. Ciobâcă, S. Delaune, and S. Kremer. Computing knowledge in security protocols under convergent equational theories. Journal of Automated Reasoning, 48(2):219--262, February 2012.
doi: 10.1007/s10817-010-9197-7.
[ BibTex | DOI | Web page | PDF ]
[Gou12]: J. Goubault-Larrecq. QRB-Domains and the Probabilistic Powerdomain. Logical Methods in Computer Science, 8(1:14), 2012.
doi: 10.2168/LMCS-8(1:14)2012.
[ BibTex | DOI | Web page | PDF ]
[DDS12]: M. Dahl, S. Delaune, and G. Steel. Formal Analysis of Privacy for Anonymous Location Based Services. In Revised Selected Papaers of the Workshop on Theory of Security and Applications (TOSCA'11), volume 6993 of Lecture Notes in Computer Science, pages 98--112, Saarbrücken, Germany, January 2012. Springer.
doi: 10.1007/978-3-642-27375-9_6.
[ BibTex | DOI | Web page | PDF ]
[AGG12]: A. Adjé, S. Gaubert, and É. Goubault. Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis. Logical Methods in Computer Science, 8(1:1), January 2012.
doi: 10.2168/LMCS-8(1:01)2012.
[ BibTex | DOI | Web page | PDF ]
[ACD11b]: M. Arnaud, V. Cortier, and S. Delaune. Modeling and Verifying Ad Hoc Routing Protocols. Research Report LSV-11-24, Laboratoire Spécification et Vérification, ENS Cachan, France, December 2011. 66 pages.
[ BibTex | Web page | PDF ]
[Arn11]: M. Arnaud. Formal verification of secured routing protocols. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, December 2011.
[ BibTex | Web page | PDF ]
[Cio11a]: S. Ciobâcă. Automated Verification of Security Protocols with Appplications to Electronic Voting. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, December 2011.
[ BibTex | Web page | PDF ]
[ILV11]: M. Izabachène, B. Libert, and D. Vergnaud. Block-wise P-Signatures and Non-Interactive Anonymous Credentials with Efficient Attributes. In Proceedings of the 13th IMA International Conference on Cryptography and Coding (IMACC'11), volume 7089 of Lecture Notes in Computer Science, pages 431--450, Oxford, UK, December 2011. Springer.
doi: 10.1007/978-3-642-25516-8_26.
[ BibTex | DOI | Web page | PDF ]
[CDK11]: C. Chevalier, S. Delaune, and S. Kremer. Transforming Password Protocols to Compose. In Proceedings of the 31st Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'11), volume 13 of Leibniz International Proceedings in Informatics, pages 204--216, Mumbai, India, December 2011. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.FSTTCS.2011.204.
[ BibTex | DOI | Web page | PDF ]
[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), pages 321--330, Chicago, Illinois, USA, October 2011. ACM Press.
doi: 10.1145/2046707.2046744.
[ BibTex | DOI | Web page | PDF ]
[CSV11a]: R. Chadha, A. P. Sistla, and M. Viswanathan. Power of Randomization in Automata on Infinite Strings. Logical Methods in Computer Science, 7(3:22), September 2011.
doi: 10.2168/LMCS-7(3:22)2011.
[ BibTex | DOI | Web page | PDF ]
[Pas11]: D. Pasailă. Verifying equivalence properties of security protocols. Rapport de Master, Master Parisien de Recherche en Informatique, Paris, France, September 2011.
[ BibTex | Web page | PDF ]
[Deg11]: J. Degrieck. Réduction de graphes pour l'analyse de protocoles de routage sécurisés. Rapport de Master, Master Parisien de Recherche en Informatique, Paris, France, September 2011.
[ BibTex | Web page | PDF ]
[FLS11]: R. Focardi, F. L. Luccio, and G. Steel. An Introduction to Security API Analysis. In Foundations of Security Analysis and Design -- FOSAD Tutorial Lectures (FOSAD'VI), volume 6858 of Lecture Notes in Computer Science, pages 35--65. Springer, September 2011.
doi: 10.1007/978-3-642-23082-0_2.
[ BibTex | DOI | Web page | PDF ]
[CKV⁺11]: R. Chadha, V. Korthikranthi, M. Viswanathan, G. Agha, and 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), pages 121--130, Aachen, Germany, September 2011. IEEE Computer Society Press.
doi: 10.1109/QEST.2011.22.
[ BibTex | DOI | Web page | PDF ]
[Gou11a]: J. Goubault-Larrecq. A Few Pearls in the Theory of Quasi-Metric Spaces. Invited talk, Fifth International Conference on Topology, Algebra, and Categories in Logic (TACL'11), Marseilles, France, July 2011, July 2011.
[ BibTex ]
[LPS11]: F. Luccio, L. Pagli, and G. Steel. Mathematical and Algorithmic Foundations of the Internet. CRC Press, July 2011.
[ BibTex | Web page ]
[Cio11b]: S. Ciobâcă. Computing finite variants for subterm convergent rewrite systems. In Proceedings of the 25th International Workshop on Unification (UNIF'11), Wroclaw, Poland, July 2011.
[ BibTex | Web page | PDF ]
[ACD11a]: M. Arnaud, V. Cortier, and S. 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, Wroclaw, Poland, July 2011. Springer.
doi: 10.1007/978-3-642-22438-6_6.
[ BibTex | DOI | Web page | PDF ]
[GK11]: J. Goubault-Larrecq and K. Keimel. Choquet-Kendall-Matheron Theorems for Non-Hausdorff Spaces. Mathematical Structures in Computer Science, 21(3):511--561, June 2011.
doi: 10.1017/S0960129510000617.
[ BibTex | DOI | Web page | PDF ]
[BCJ⁺11]: M. Backes, I. Cervesato, A. Jaggard, A. Scedrov, and J.-K. Tsay. Cryptographically sound security proofs for basic and public-key Kerberos. International Journal on Information Security, 10(2):107--134, June 2011.
doi: 10.1007/s10207-011-0125-6.
[ BibTex | DOI | Web page | PDF ]
[KSW11]: S. Kremer, G. Steel, and B. Warinschi. Security for Key Management Interfaces. In Proceedings of the 24th IEEE Computer Security Foundations Symposium (CSF'11), pages 266--280, Cernay-la-Ville, France, June 2011. IEEE Computer Society Press.
doi: 10.1109/CSF.2011.25.
[ BibTex | DOI | Web page | PDF ]
[DKRS11]: S. Delaune, S. Kremer, M. D. Ryan, and G. Steel. Formal analysis of protocols based on TPM state registers. In Proceedings of the 24th IEEE Computer Security Foundations Symposium (CSF'11), pages 66--82, Cernay-la-Ville, France, June 2011. IEEE Computer Society Press.
doi: 10.1109/CSF.2011.12.
[ BibTex | DOI | Web page | PDF ]
[GV11]: J. Goubault-Larrecq and D. Varacca. Continuous Random Variables. In Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science (LICS'11), pages 97--106, Toronto, Canada, June 2011. IEEE Computer Society Press.
doi: 10.1109/LICS.2011.23.
[ BibTex | DOI | Web page | PDF ]
[Ben11]: H. Benzina. Logic in Virtualized Systems. In Proceedings of the International Conference on Computer Applications and Network Security (ICCANS'11), Republic of Maldives, May 2011.
[ BibTex | Web page | PDF ]
[Gou11b]: J. Goubault-Larrecq. Musings Around the Geometry of Interaction, and Coherence. Theoretical Computer Science, 412(20):1998--2014, April 2011.
doi: 10.1016/j.tcs.2010.12.023.
[ BibTex | DOI | Web page | PDF ]
[JKV11]: F. Jacquemard, F. Klay, and C. Vacher. Rigid Tree Automata. Information and Computation, 209(3):486--512, March 2011.
doi: 10.1016/j.ic.2010.11.015.
[ BibTex | DOI | Web page | PDF ]
[CC11]: H. Comon-Lundh and 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), volume 9 of Leibniz International Proceedings in Informatics, pages 29--44, Dortmund, Germany, March 2011. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.STACS.2011.29.
[ BibTex | DOI | Web page | PDF ]
[Kre11]: S. Kremer. Modelling and analyzing security protocols in cryptographic process calculi. Mémoire d'habilitation, École Normale Supérieure de Cachan, France, March 2011.
[ BibTex | Web page | PDF ]
[Ste11b]: G. Steel. Formal Analysis of Security APIs. Mémoire d'habilitation, École Normale Supérieure de Cachan, France, March 2011.
[ BibTex | Web page | PDF ]
[Del11]: S. Delaune. Verification of security protocols: from confidentiality to privacy. Mémoire d'habilitation, École Normale Supérieure de Cachan, France, March 2011.
[ BibTex | Web page | PDF ]
[ACGP11]: M. Abdalla, C. Chevalier, L. Granboulan, and 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), volume 6558 of Lecture Notes in Computer Science, pages 142--160, San Francisco, California, USA, February 2011. Springer.
doi: 10.1007/978-3-642-19074-2_11.
[ BibTex | DOI | Web page | PDF ]
[CSV11b]: R. Chadha, A. P. Sistla, and 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), volume 6538 of Lecture Notes in Computer Science, pages 103--117, Austin, Texas, USA, January 2011. Springer.
doi: 10.1007/978-3-642-18275-4_9.
[ BibTex | DOI | Web page | PDF ]
[Ste11a]: G. Steel. Formal Analysis of Security APIs. In Encyclopedia of Cryptography and Security, pages 492--494. Springer, 2nd edition, 2011.
doi: 10.1007/978-1-4419-5906-5_873.
[ BibTex | DOI ]
[CDM11]: H. Comon-Lundh, S. Delaune, and J. K. Millen. Constraint solving techniques and enriching the model with equational theories. In Formal Models and Techniques for Analyzing Security Protocols, volume 5 of Cryptology and Information Security Series, pages 35--61. IOS Press, 2011.
[ BibTex | Web page | PDF ]
[CK11]: V. Cortier and S. Kremer, editors. Formal Models and Techniques for Analyzing Security Protocols, volume 5 of Cryptology and Information Security Series. IOS Press, 2011.
[ BibTex | Web page ]
[CSV10]: R. Chadha, A. P. Sistla, and 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), volume 8 of Leibniz International Proceedings in Informatics, pages 364--375, Chennai, India, December 2010. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.FSTTCS.2010.364.
[ BibTex | DOI | Web page | PDF ]
[DKS10]: S. Delaune, S. Kremer, and G. Steel. Formal Analysis of PKCS#11 and Proprietary Extensions. Journal of Computer Security, 18(6):1211--1245, November 2010.
doi: 10.3233/JCS-2009-0394.
[ BibTex | DOI | Web page | PDF ]
[Gou10b]: J. Goubault-Larrecq. Finite Models for Formal Security Proofs. Journal of Computer Security, 18(6):1247--1299, November 2010.
doi: 10.3233/JCS-2009-0395.
[ BibTex | DOI | Web page | PDF ]
[KM10]: S. Kremer and L. Mazaré. Computationally Sound Analysis of Protocols using Bilinear Pairings. Journal of Computer Security, 18(6):999--1033, November 2010.
doi: 10.3233/JCS-2009-0388.
[ BibTex | DOI | Web page | PDF ]
[LMT10]: R. Lanotte, A. Maggiolo-Schettini, and A. Troina. Weak bisimulation for Probabilistic Timed Automata? Theoretical Computer Science, 411(50):4291--4322, November 2010.
doi: 10.1016/j.tcs.2010.09.003.
[ BibTex | DOI | Web page | PDF ]
[BCFS10]: M. Bortolozzo, M. Centenaro, R. Focardi, and G. Steel. Attacking and Fixing PKCS#11 Security Tokens. In Proceedings of the 17th ACM Conference on Computer and Communications Security (CCS'10), pages 260--269, Chicago, Illinois, USA, October 2010. ACM Press.
doi: 10.1145/1866307.1866337.
[ BibTex | DOI | Web page | PDF ]
[SRKK10]: B. Smyth, M. D. Ryan, S. Kremer, and M. Kourjieh. Towards automatic analysis of election verifiability properties. In Proceedings of the Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security (ARSPA-WITS'10), volume 6186 of Lecture Notes in Computer Science, pages 146--163, Paphos, Cyprus, October 2010. Springer.
doi: 10.1007/978-3-642-16074-5_11.
[ BibTex | DOI | Web page | PDF ]
[Sce10]: G. Scerri. Modélisation des clés de l'intrus. Rapport de Master, Master Parisien de Recherche en Informatique, Paris, France, September 2010.
[ BibTex ]
[BGGP10]: O. Bouissou, É. Goubault, J. Goubault-Larrecq, and 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 2010.
[ BibTex ]
[DKRS10a]: S. Delaune, S. Kremer, M. D. Ryan, and 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), volume 6561 of Lecture Notes in Computer Science, pages 111--125, Pisa, Italy, September 2010. Springer.
doi: 10.1007/978-3-642-19751-2_8.
[ BibTex | DOI | Web page | PS | PDF ]
[BWA10]: M. Baudet, B. Warinschi, and M. Abadi. Guessing Attacks and the Computational Soundness of Static Equivalence. Journal of Computer Security, 18(5):909--968, September 2010.
doi: 10.3233/JCS-2009-0386.
[ BibTex | DOI | Web page | PDF ]
[BG10]: H. Benzina and 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), volume 6514 of Lecture Notes in Computer Science, pages 244--258, Athens, Greece, September 2010. Springer.
doi: 10.1007/978-3-642-19348-4_18.
[ BibTex | DOI | Web page | PDF ]
[KRS10]: S. Kremer, M. D. Ryan, and B. Smyth. Election verifiability in electronic voting protocols. In Proceedings of the 15th European Symposium on Research in Computer Security (ESORICS'10), volume 6345 of Lecture Notes in Computer Science, pages 389--404, Athens, Greece, September 2010. Springer.
doi: 10.1007/978-3-642-15497-3_24.
[ BibTex | DOI | Web page | PDF ]
[DDS10a]: M. Dahl, S. Delaune, and G. Steel. Formal Analysis of Privacy for Vehicular Mix-Zones. In Proceedings of the 15th European Symposium on Research in Computer Security (ESORICS'10), volume 6345 of Lecture Notes in Computer Science, pages 55--70, Athens, Greece, September 2010. Springer.
doi: 10.1007/978-3-642-15497-3_4.
[ BibTex | DOI | Web page | PS | PDF ]
[DKRS10b]: S. Delaune, S. Kremer, M. D. Ryan, and G. Steel. A Formal Analysis of Authentication in the TPM (short paper). In Preliminary Proceedings of the 8th International Workshop on Security Issues in Coordination Models, Languages and Systems (SecCo'10), Paris, France, August 2010.
[ BibTex | Web page | PS | PDF ]
[Car10]: J.-L. Carré. Analyse statique de programmes multi-thread pour l'embarqué. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, July 2010.
[ BibTex | Web page | PDF ]
[DDS10b]: M. Dahl, S. Delaune, and G. Steel. Formal Analysis of Privacy for Vehicular Mix-Zones. In Proceedings of the Workshop on Foundations of Security and Privacy (FCS-PrivMod'10), pages 55--70, Edinburgh, Scotland, UK, July 2010.
doi: 10.1007/978-3-642-15497-3_4.
[ BibTex | DOI | Web page | PS | PDF ]
[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), volume 6173 of Lecture Notes in Artificial Intelligence, pages 412--426, Edinburgh, Scotland, UK, July 2010. Springer-Verlag.
doi: 10.1007/978-3-642-14203-1_35.
[ BibTex | DOI | Web page | PDF ]
[Gou10c]: J. Goubault-Larrecq. Noetherian Spaces in Verification. In Proceedings of the 37th International Colloquium on Automata, Languages and Programming (ICALP'10) -- Part II, volume 6199 of Lecture Notes in Computer Science, pages 2--21, Bordeaux, France, July 2010. Springer.
doi: 10.1007/978-3-642-14162-1_2.
[ BibTex | DOI | Web page | PDF ]
[CC10]: S. Ciobâcă and V. Cortier. Protocol composition for arbitrary primitives. In Proceedings of the 23rd IEEE Computer Security Foundations Symposium (CSF'10), pages 322--336, Edinburgh, Scotland, UK, July 2010. IEEE Computer Society Press.
doi: 10.1109/CSF.2010.29.
[ BibTex | DOI | Web page | PDF ]
[ACD10]: M. Arnaud, V. Cortier, and S. Delaune. Modeling and Verifying Ad Hoc Routing Protocols. In Proceedings of the 23rd IEEE Computer Security Foundations Symposium (CSF'10), pages 59--74, Edinburgh, Scotland, UK, July 2010. IEEE Computer Society Press.
doi: 10.1109/CSF.2010.12.
[ BibTex | DOI | Web page | PDF ]
[Gou10d]: J. Goubault-Larrecq. ωQRB-Domains and the Probabilistic Powerdomain. In Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science (LICS'10), pages 352--361, Edinburgh, Scotland, UK, July 2010. IEEE Computer Society Press.
doi: 10.1109/LICS.2010.50.
[ BibTex | DOI | Web page | PDF ]
[DKR10b]: S. Delaune, S. Kremer, and M. D. Ryan. Verifying Privacy-Type Properties of Electronic Voting Protocols: A Taster. In Towards Trustworthy Elections -- New Directions in Electronic Voting, volume 6000 of Lecture Notes in Computer Science, pages 289--309. Springer, May 2010.
doi: 10.1007/978-3-642-12980-3_18.
[ BibTex | DOI | Web page | PDF ]
[Gou10a]: J. Goubault-Larrecq. De Groot Duality and Models of Choice: Angels, Demons, and Nature. Mathematical Structures in Computer Science, 20(2):169--237, April 2010.
doi: 10.1017/S0960129509990363.
[ BibTex | DOI | Web page | PDF ]
[CKW10]: V. Cortier, S. Kremer, and B. Warinschi. A Survey of Symbolic Methods in Computational Analysis of Cryptographic Systems. Journal of Automated Reasoning, 46(3-4):225--259, April 2010.
doi: 10.1007/s10817-010-9187-9.
[ BibTex | DOI | Web page | PDF ]
[DKR10a]: S. Delaune, S. Kremer, and M. D. Ryan. Symbolic bisimulation for the applied pi calculus. Journal of Computer Security, 18(2):317--377, March 2010.
doi: 10.3233/JCS-2010-0363.
[ BibTex | DOI | Web page | PDF ]
[CCZ10]: H. Comon-Lundh, V. Cortier, and E. Zălinescu. Deciding security properties for cryptographic protocols. Application to key cycles. ACM Transactions on Computational Logic, 11(2), January 2010.
doi: 10.1145/1656242.1656244.
[ BibTex | DOI | Web page | PDF ]
[Mer09]: A. Mercier. Contributions à l'analyse automatique des protocoles cryptographiques en présence de propriétés algébriques : protocoles de groupe, équivalence statique. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, December 2009.
[ BibTex | Web page | PDF ]
[Bur09a]: S. Bursuc. Contraintes de déductibilité dans une algèbre quotient: réduction de modèles et applications à la sécurité. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, December 2009.
[ BibTex | Web page | PDF ]
[Gou09a]: J. Goubault-Larrecq. Logic Wins!. In Proceedings of the 13th Asian Computing Science Conference (ASIAN'09), volume 5913 of Lecture Notes in Computer Science, pages 1--16, Seoul, Korea, December 2009. Springer.
doi: 10.1007/978-3-642-10622-4_1.
[ BibTex | DOI | Web page | PDF ]
[DKP09]: S. Delaune, S. Kremer, and O. Pereira. Simulation based security in the applied pi calculus. In Proceedings of the 29th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'09), volume 4 of Leibniz International Proceedings in Informatics, pages 169--180, Kanpur, India, December 2009. Leibniz-Zentrum für Informatik.
doi: 10.4230/LIPIcs.FSTTCS.2009.2316.
[ BibTex | DOI | Web page | PDF ]
[KMT09a]: S. Kremer, A. Mercier, and R. Treinen. Reducing Equational Theories for the Decision of Static Equivalence. In Proceedings of the 13th Asian Computing Science Conference (ASIAN'09), volume 5913 of Lecture Notes in Computer Science, pages 94--108, Seoul, Korea, December 2009. Springer.
doi: 10.1007/978-3-642-10622-4_8.
[ BibTex | DOI | Web page | PS | PDF ]
[BDC09]: S. Bursuc, S. Delaune, and H. Comon-Lundh. Deducibility constraints. In Proceedings of the 13th Asian Computing Science Conference (ASIAN'09), volume 5913 of Lecture Notes in Computer Science, pages 24--38, Seoul, Korea, December 2009. Springer.
doi: 10.1007/978-3-642-10622-4_3.
[ BibTex | DOI | Web page | PS | PDF ]
[SRKK09]: B. Smyth, M. D. Ryan, S. Kremer, and M. Kourjieh. Election verifiability in electronic voting protocols (Preliminary version). In Proceedings of the 4th Benelux Workshop on Information and System Security (WISSEC'09), Louvain-la-Neuve, Belgium, November 2009.
[ BibTex | Web page | PDF ]
[Ste09b]: G. Steel. Towards a Formal Analysis of the SeVeCoM API. In Proceedings of the 7th Conference on Embedded Security in Cars (ESCAR'09), Düsseldorf, Germany, November 2009.
[ BibTex | Web page | PDF ]
[CCD09]: V. Cheval, H. Comon-Lundh, and S. Delaune. A decision procedure for proving observational equivalence. In Preliminary Proceedings of the 7th International Workshop on Security Issues in Coordination Models, Languages and Systems (SecCo'09), Bologna, Italy, October 2009.
[ BibTex | Web page | PDF ]
[FLS09]: R. Focardi, F. L. Luccio, and G. Steel. Blunting Differential Attacks on PIN Processing APIs. In Proceedings of the 14th Nordic Workshop on Secure IT Systems (NordSec'09), volume 5838 of Lecture Notes in Computer Science, pages 88--103, Oslo, Norway, October 2009. Springer.
doi: 10.1007/978-3-642-04766-4_7.
[ BibTex | DOI | Web page | PDF ]
[Che09]: V. Cheval. Algorithme de décision de l'équivalence symbolique de systèmes de contraintes. Rapport de Master, Master Parisien de Recherche en Informatique, Paris, France, September 2009.
[ BibTex | Web page | PDF ]
[CFLS09]: M. Centenaro, R. Focardi, F. L. Luccio, and G. Steel. Type-based Analysis of PIN Processing APIs. In Proceedings of the 14th European Symposium on Research in Computer Security (ESORICS'09), volume 5789 of Lecture Notes in Computer Science, pages 53--68, Saint Malo, France, September 2009. Springer.
doi: 10.1007/978-3-642-04444-1_4.
[ BibTex | DOI | Web page | PDF ]
[CS09]: V. Cortier and G. 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), volume 5789 of Lecture Notes in Computer Science, pages 605--620, Saint Malo, France, September 2009. Springer.
doi: 10.1007/978-3-642-04444-1_37.
[ BibTex | DOI | Web page | PDF ]
[CC09]: S. Ciobâcă and V. Cortier. Algorithmes pour l'équivalence statique. Deliverable AVOTE 2.1 (ANR-07-SESU-002), September 2009. 17 pages.
[ BibTex | Web page | PDF ]
[BK09]: M. Boreale and S. Kremer, editors. Proceedings of the 7th International Workshop on Security Issues in Concurrency (SecCo'09), volume 7 of Electronic Proceedings in Theoretical Computer Science, Bologna, Italy, August 2009.
doi: 10.4204/EPTCS.7.
[ BibTex | DOI | Web page ]
[KAS09]: G. Keighren, D. Aspinall, and G. Steel. Towards a Type System for Security APIs. In Revised Selected Papers of the Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security (ARSPA-WITS'09), volume 5511 of Lecture Notes in Computer Science, pages 173--192, York, UK, August 2009. Springer.
doi: 10.1007/978-3-642-03459-6_12.
[ BibTex | DOI | Web page | PDF ]
[FS09]: S. Fröschle and G. Steel. Analysing PKCS#11 Key Management APIs with Unbounded Fresh Data. In Revised Selected Papers of the Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security (ARSPA-WITS'09), volume 5511 of Lecture Notes in Computer Science, pages 92--106, York, UK, August 2009. Springer.
doi: 10.1007/978-3-642-03459-6_7.
[ BibTex | DOI | Web page | PDF ]
[CDK09c]: S. Ciobâcă, S. Delaune, and S. Kremer. Computing knowledge in security protocols under convergent equational theories. In Proceedings of the 22nd International Conference on Automated Deduction (CADE'09), volume 5663 of Lecture Notes in Computer Science, pages 355--370, Montreal, Canada, August 2009. Springer.
doi: 10.1007/978-3-642-02959-2_27.
[ BibTex | DOI | Web page | PDF ]
[KP09]: S. Kremer and P. Panangaden, editors. Proceedings of the 6th International Workshop on Security Issues in Concurrency (SecCo'08), volume 242 of Electronic Notes in Theoretical Computer Science, Toronto, Canada, August 2009. Elsevier Science Publishers.
doi: 10.1016/j.entcs.2009.07.077.
[ BibTex | DOI | Web page ]
[DKR09]: S. Delaune, S. Kremer, and M. D. Ryan. Verifying Privacy-type Properties of Electronic Voting Protocols. Journal of Computer Security, 17(4):435--487, July 2009.
doi: 10.3233/JCS-2009-0340.
[ BibTex | DOI | Web page | PS | PDF ]
[HN09]: P.-C. Héam and C. Nicaud. Seed: an Easy-to-Use Random Generator of Recursive Data Structures for Testing. Research Report LSV-09-15, Laboratoire Spécification et Vérification, ENS Cachan, France, July 2009. 16 pages.
[ BibTex | Web page | PDF ]
[CDK09b]: S. Ciobâcă, S. Delaune, and S. Kremer. Computing knowledge in security protocols under convergent equational theories. In Preliminary Proceedings of the 4th International Workshop on Security and Rewriting Techniques (SecReT'09), pages 47--58, Port Jefferson, New York, USA, July 2009.
[ BibTex | Web page | PDF ]
[ACD09]: M. Arnaud, V. Cortier, and S. Delaune. Modeling and Verifying Ad Hoc Routing Protocol. In Preliminary Proceedings of the 4th International Workshop on Security and Rewriting Techniques (SecReT'09), pages 33--46, Port Jefferson, New York, USA, July 2009.
[ BibTex | Web page | PS | PDF ]
[KMT09b]: S. Kremer, A. Mercier, and R. Treinen. Reducing Equational Theories for the Decision of Static Equivalence (Preliminary Version). In Preliminary Proceedings of the 4th International Workshop on Security and Rewriting Techniques (SecReT'09), Port Jefferson, New York, USA, July 2009.
[ BibTex | Web page | PS | PDF ]
[FG09b]: A. Finkel and J. Goubault-Larrecq. Forward Analysis for WSTS, Part II: Complete WSTS. In Proceedings of the 36th International Colloquium on Automata, Languages and Programming (ICALP'09), volume 5556 of Lecture Notes in Computer Science, pages 188--199, Rhodes, Greece, July 2009. Springer.
doi: 10.1007/978-3-642-02930-1_16.
[ BibTex | DOI | Web page | PDF ]
[CD09a]: V. Cortier and S. Delaune. A method for proving observational equivalence. In Proceedings of the 22nd IEEE Computer Security Foundations Symposium (CSF'09), pages 266--276, Port Jefferson, New York, USA, July 2009. IEEE Computer Society Press.
doi: 10.1109/CSF.2009.9.
[ BibTex | DOI | Web page | PDF ]
[Ste09a]: G. Steel. Computational Soundness for APIs. In Proceedings of the 5th Workshop on Formal and Computational Cryptography (FCC'09), Port Jefferson, New York, USA, July 2009.
[ BibTex | Web page | PDF ]
[ABC09]: M. Abadi, B. Blanchet, and H. Comon-Lundh. Models and Proofs of Protocol Security: A Progress Report. In Proceedings of the 21st International Conference on Computer Aided Verification (CAV'09), volume 5643 of Lecture Notes in Computer Science, pages 35--49, Grenoble, France, June-July 2009. Springer.
doi: 10.1007/978-3-642-02658-4_5.
[ BibTex | DOI | Web page | PDF ]
[CDK09a]: R. Chadha, S. Delaune, and S. Kremer. Epistemic Logic for the Applied Pi Calculus. In Proceedings of IFIP International Conference on Formal Techniques for Distributed Systems (FMOODS/FORTE'09), volume 5522 of Lecture Notes in Computer Science, pages 182--197, Lisbon, Portugal, June 2009. Springer.
doi: 10.1007/978-3-642-02138-1_12.
[ BibTex | DOI | Web page | PS | PDF ]
[BC09a]: S. Bursuc and H. Comon-Lundh. Protocol security and algebraic properties: decision results for a bounded number of sessions. In Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA'09), volume 5595 of Lecture Notes in Computer Science, pages 133--147, Brasília, Brazil, June-July 2009. Springer.
doi: 10.1007/978-3-642-02348-4_10.
[ BibTex | DOI | Web page | PDF ]
[BCD09]: M. Baudet, V. Cortier, and S. Delaune. YAPA: A generic tool for computing intruder knowledge. In Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA'09), volume 5595 of Lecture Notes in Computer Science, pages 148--163, Brasília, Brazil, June-July 2009. Springer.
doi: 10.1007/978-3-642-02348-4_11.
[ BibTex | DOI | Web page | PDF ]
[AC09]: R. Affeldt and H. Comon-Lundh. Verification of Security Protocols with a Bounded Number of Sessions Based on Resolution for Rigid Variables. In Formal to Practical Security, volume 5458 of Lecture Notes in Computer Science, pages 1--20. Springer, May 2009.
doi: 10.1007/978-3-642-02002-5_1.
[ BibTex | DOI | Web page | PDF ]
[Gou09b]: J. Goubault-Larrecq. On a Generalization of a Result by Valk and Jantzen. Research Report LSV-09-09, Laboratoire Spécification et Vérification, ENS Cachan, France, May 2009. 18 pages.
[ BibTex | Web page | PDF ]
[Bur09b]: E. Bursztein. Extending Anticipation Games with Location, Penalty and Timeline. In Revised Selected Papers of the 5th International Workshop on Formal Aspects in Security and Trust (FAST'08), volume 5491 of Lecture Notes in Computer Science, pages 272--286, Malaga, Spain, April 2009. Springer.
doi: 10.1007/978-3-642-01465-9_18.
[ BibTex | DOI | Web page | PDF ]
[JKV09]: F. Jacquemard, F. Klay, and C. Vacher. Rigid Tree Automata. In Proceedings of the 3rd International Conference on Language and Automata Theory and Applications (LATA'09), volume 5457 of Lecture Notes in Computer Science, pages 446--457, Tarragona, Spain, April 2009. Springer.
doi: 10.1007/978-3-642-00982-2_38.
[ BibTex | DOI | Web page | PDF ]
[BCK09]: M. Baudet, V. Cortier, and S. Kremer. Computationally Sound Implementations of Equational Theories against Passive Adversaries. Information and Computation, 207(4):496--520, April 2009.
doi: 10.1016/j.ic.2008.12.005.
[ BibTex | DOI | Web page | PDF ]
[CD09b]: V. Cortier and S. Delaune. Safely Composing Security Protocols. Formal Methods in System Design, 34(1):1--36, February 2009.
doi: 10.1007/s10703-008-0059-4.
[ BibTex | DOI | Web page | PS | PDF ]
[BC09b]: S. Bursuc and H. Comon-Lundh. Protocols, insecurity decision and combination of equational theories. Research Report LSV-09-02, Laboratoire Spécification et Vérification, ENS Cachan, France, February 2009. 43 pages.
[ BibTex | Web page | PDF ]
[FG09a]: A. Finkel and J. Goubault-Larrecq. Forward Analysis for WSTS, Part I: Completions. In Proceedings of the 26th Annual Symposium on Theoretical Aspects of Computer Science (STACS'09), volume 3 of Leibniz International Proceedings in Informatics, pages 433--444, Freiburg, Germany, February 2009. Leibniz-Zentrum für Informatik.
[ BibTex | Web page | PDF ]
[Com08a]: H. Comon-Lundh. About models of security protocols. In Proceedings of the 28th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'08), volume 2 of Leibniz International Proceedings in Informatics, Bangalore, India, December 2008. Leibniz-Zentrum für Informatik.
[ BibTex | Web page | PDF ]
[GLN08]: J. Goubault-Larrecq, S. Lasota, and D. Nowak. Logical Relations for Monadic Types. Mathematical Structures in Computer Science, 18(6):1169--1217, December 2008. 81 pages.
doi: 10.1017/S0960129508007172.
[ BibTex | DOI | Web page | PDF ]
[Bur08a]: E. Bursztein. Anticipation games. Théorie des jeux appliqués à la sécurité réseau. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, November 2008.
[ BibTex | Web page | PDF ]
[Ara08]: M. Arapinis. Sécurité des protocoles cryptographiques : décidabilité et résultats de réduction. Thèse de doctorat, Université Paris 12, Créteil, France, November 2008.
[ BibTex | Web page | PDF ]
[ADK08]: M. Arapinis, S. Delaune, and S. Kremer. From One Session to Many: Dynamic Tags for Security Protocols. In Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'08), volume 5330 of Lecture Notes in Artificial Intelligence, pages 128--142, Doha, Qatar, November 2008. Springer.
doi: 10.1007/978-3-540-89439-1_9.
[ BibTex | DOI | Web page | PDF ]
[CC08]: H. Comon-Lundh and V. Cortier. Computational Soundness of Observational Equivalence. In Proceedings of the 15th ACM Conference on Computer and Communications Security (CCS'08), pages 109--118, Alexandria, Virginia, USA, October 2008. ACM Press.
doi: 10.1145/1455770.1455786.
[ BibTex | DOI | Web page | PDF ]
[Bur08c]: E. Bursztein. NetQi: A Model Checker for Anticipation Game. In Proceedings of the 6th International Symposium on Automated Technology for Verification and Analysis (ATVA'08), volume 5311 of Lecture Notes in Computer Science, pages 246--251, Seoul, Korea, October 2008. Springer.
doi: 10.1007/978-3-540-88387-6_22.
[ BibTex | DOI | Web page | PDF ]
[Cio08]: S. Ciobâcă. Verification of anonymity properties in e-voting protocols. Rapport de Master, Master Parisien de Recherche en Informatique, Paris, France, September 2008.
[ BibTex | Web page | PDF ]
[Sch08]: Ph. Schnoebelen. The complexity of lossy channel systems. Invited talk, Workshop Automata and Verification (AV'08), Mons, Belgium, August 2008.
[ BibTex ]
[Com08b]: H. Comon-Lundh. Challenges in the Automated Verification of Security Protocols. In Proceedings of the 4th International Joint Conference on Automated Reasoning (IJCAR'08), volume 5195 of Lecture Notes in Artificial Intelligence, pages 396--409, Sydney, Australia, August 2008. Springer-Verlag.
doi: 10.1007/978-3-540-71070-7_34.
[ BibTex | DOI | Web page | PDF ]
[KMT08]: S. Kremer, A. Mercier, and R. Treinen. Proving Group Protocols Secure Against Eavesdroppers. In Proceedings of the 4th International Joint Conference on Automated Reasoning (IJCAR'08), volume 5195 of Lecture Notes in Artificial Intelligence, pages 116--131, Sydney, Australia, August 2008. Springer-Verlag.
doi: 10.1007/978-3-540-71070-7_9.
[ BibTex | DOI | Web page | PDF ]
[Gou08a]: J. Goubault-Larrecq. A Cone-Theoretic Krein-Milman Theorem. Research Report LSV-08-18, Laboratoire Spécification et Vérification, ENS Cachan, France, June 2008. 8 pages.
[ BibTex | Web page | PDF ]
[CJP08]: H. Comon-Lundh, F. Jacquemard, and N. Perrin. Visibly Tree Automata with Memory and Constraints. Logical Methods in Computer Science, 4(2:8), June 2008.
doi: 10.2168/LMCS-4(2:8)2008.
[ BibTex | DOI | Web page | PDF ]
[Gou08d]: J. Goubault-Larrecq. Towards Producing Formally Checkable Security Proofs, Automatically. In Proceedings of the 21st IEEE Computer Security Foundations Symposium (CSF'08), pages 224--238, Pittsburgh, Pennsylvania, USA, June 2008. IEEE Computer Society Press.
doi: 10.1109/CSF.2008.21.
[ BibTex | DOI | Web page | PDF ]
[DKR08]: S. Delaune, S. Kremer, and M. D. Ryan. Composition of Password-based Protocols. In Proceedings of the 21st IEEE Computer Security Foundations Symposium (CSF'08), pages 239--251, Pittsburgh, Pennsylvania, USA, June 2008. IEEE Computer Society Press.
doi: 10.1109/CSF.2008.6.
[ BibTex | DOI | Web page | PDF ]
[DKS08a]: S. Delaune, S. Kremer, and G. Steel. Formal Analysis of PKCS#11. In Proceedings of the 21st IEEE Computer Security Foundations Symposium (CSF'08), pages 331--344, Pittsburgh, Pennsylvania, USA, June 2008. IEEE Computer Society Press.
doi: 10.1109/CSF.2008.16.
[ BibTex | DOI | Web page | PDF ]
[DRS08]: S. Delaune, M. D. Ryan, and B. Smyth. Automatic verification of privacy properties in the applied pi-calculus. In Proceedings of the 2nd Joint iTrust and PST Conferences on Privacy, Trust Management and Security (IFIPTM'08), volume 263 of IFIP Conference Proceedings, pages 263--278, Trondheim, Norway, June 2008. Springer.
[ BibTex | Web page | PS | PDF ]
[Bur08e]: E. Bursztein. Probabilistic Protocol Identification for Hard to Classify Protocol. In Proceedings of the 2nd International Workshop on Information Security Theory and Practices (WISTP'08), volume 5019 of Lecture Notes in Computer Science, pages 49--63, Sevilla, Spain, May 2008. Springer. Best paper award.
doi: 10.1007/978-3-540-79966-5_4.
[ BibTex | DOI | Web page | PDF ]
[JRV08]: F. Jacquemard, M. Rusinowitch, and L. Vigneron. Tree automata with equality constraints modulo equational theories. Journal of Logic and Algebraic Programming, 75(2):182--208, April 2008.
doi: 10.1016/j.jlap.2007.10.006.
[ BibTex | DOI | Web page | PDF ]
[Gou08c]: J. Goubault-Larrecq. Simulation Hemi-Metrics Between Infinite-State Stochastic Games. In Proceedings of the 11th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'08), volume 4962 of Lecture Notes in Computer Science, pages 50--65, Budapest, Hungary, March-April 2008. Springer.
doi: 10.1007/978-3-540-78499-9_5.
[ BibTex | DOI | Web page ]
[Gou08b]: J. Goubault-Larrecq. Prevision Domains and Convex Powercones. In Proceedings of the 11th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'08), volume 4962 of Lecture Notes in Computer Science, pages 318--333, Budapest, Hungary, March-April 2008. Springer.
doi: 10.1007/978-3-540-78499-9_23.
[ BibTex | DOI | Web page ]
[GO08]: J. Goubault-Larrecq and J. Olivain. A Smell of Orchids. In Proceedings of the 8th Workshop on Runtime Verification (RV'08), volume 5289 of Lecture Notes in Computer Science, pages 1--20, Budapest, Hungary, March 2008. Springer.
doi: 10.1007/978-3-540-89247-2_1.
[ BibTex | DOI | Web page | PDF ]
[DKS08b]: S. Delaune, S. Kremer, and G. Steel. Formal Analysis of PKCS#11. In Proceedings of the 4th Taiwanese-French Conference on Information Technology (TFIT'08), pages 267--278, Taipei, Taiwan, March 2008.
[ BibTex | Web page | PDF ]
[DLLT08]: S. Delaune, P. Lafourcade, D. Lugiez, and R. Treinen. Symbolic protocol analysis for monoidal equational theories. Information and Computation, 206(2-4):312--351, February-April 2008.
doi: 10.1016/j.ic.2007.07.005.
[ BibTex | DOI | Web page | PDF ]
[Bur08d]: E. Bursztein. Network Administrator and Intruder Strategies. Research Report LSV-08-02, Laboratoire Spécification et Vérification, ENS Cachan, France, February 2008. 23 pages.
[ BibTex | Web page | PDF ]
[PPS⁺08]: P. Papadimitratos, M. Poturalski, P. Schaller, P. Lafourcade, D. Basin, S. Čapkun, and J.-P. Hubaux. Secure Neighborhood Discovery: A Fundamental Element for Mobile Ad Hoc Networking. IEEE Communications Magazine, 46(2):132--139, February 2008.
doi: 10.1109/MCOM.2008.4473095.
[ BibTex | DOI | Web page | PDF ]
[BC08]: V. Bernat and H. Comon-Lundh. Normal proofs in intruder theories. In Revised Selected Papers of the 11th Asian Computing Science Conference (ASIAN'06), volume 4435 of Lecture Notes in Computer Science, pages 151--166, Tokyo, Japan, January 2008. Springer.
doi: 10.1007/978-3-540-77505-8_12.
[ BibTex | DOI | Web page | PDF ]
[LNY08]: S. Lasota, D. Nowak, and Z. Yu. On completeness of logical relations for monadic types. In Revised Selected Papers of the 11th Asian Computing Science Conference (ASIAN'06), volume 4435 of Lecture Notes in Computer Science, pages 223--230, Tokyo, Japan, January 2008. Springer.
doi: 10.1007/978-3-540-77505-8_17.
[ BibTex | DOI | Web page | PDF ]
[Kre08]: S. Kremer. Computational soundness of equational theories (Tutorial). In Revised Selected Papers from the 3rd Symposium on Trustworthy Global Computing (TGC'07), volume 4912 of Lecture Notes in Computer Science, pages 363--382, Sophia-Antipolis, France, 2008. Springer.
doi: 10.1007/978-3-540-78663-4.
[ BibTex | DOI | Web page | PDF ]
[CKR08]: L. Chen, S. Kremer, and M. D. Ryan, editors. Formal Protocol Verification Applied, volume 07421 of Dagstuhl Seminar Proceedings, Dagstuhl, Germany, 2008.
[ BibTex | Web page ]
[Bur08b]: E. Bursztein. NetAnalyzer v0.7.5, January 2008. Written in C and Perl (about 25000 lines).
[ BibTex ]
[BG07]: E. Bursztein and J. Goubault-Larrecq. A Logical Framework for Evaluating Network Resilience Against Faults and Attacks. In Proceedings of the 12th Asian Computing Science Conference (ASIAN'07), volume 4846 of Lecture Notes in Computer Science, pages 212--227, Doha, Qatar, December 2007. Springer.
doi: 10.1007/978-3-540-76929-3_20.
[ BibTex | DOI | Web page | PDF ]
[CDD07]: V. Cortier, J. Delaitre, and S. Delaune. Safely Composing Security Protocols. In Proceedings of the 27th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'07), volume 4855 of Lecture Notes in Computer Science, pages 352--363, New Delhi, India, December 2007. Springer.
doi: 10.1007/978-3-540-77050-3_29.
[ BibTex | DOI | Web page | PDF ]
[DKR07]: S. Delaune, S. Kremer, and M. D. Ryan. Symbolic Bisimulation for the Applied Pi-Calculus. In Proceedings of the 27th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'07), volume 4855 of Lecture Notes in Computer Science, pages 133--145, New Delhi, India, December 2007. Springer.
doi: 10.1007/978-3-540-77050-3_11.
[ BibTex | DOI | Web page | PDF ]
[Car07]: J.-L. Carré. Réécriture, confluence. Course notes, Préparation à l'agrégation, ENS Cachan, France, December 2007.
[ BibTex ]
[Bur07a]: E. Bursztein. NetQi v1rc1. Available at http://www.netqi.org/, December 2007. Written in C and Java (about 10000 lines).
[ BibTex | Web page ]
[GPT07]: J. Goubault-Larrecq, C. Palamidessi, and A. Troina. A Probabilistic Applied Pi-Calculus. In Proceedings of the 5th Asian Symposium on Programming Languages and Systems (APLAS'07), volume 4807 of Lecture Notes in Computer Science, pages 175--290, Singapore, November-December 2007. Springer.
doi: 10.1007/978-3-540-76637-7_12.
[ BibTex | DOI | Web page | PDF ]
[CDG⁺07]: H. Comon-Lundh, M. Dauchet, R. Gilleron, C. Löding, F. Jacquemard, D. Lugiez, S. Tison, and M. Tommasi. Tree Automata Techniques and Applications. November 2007.
[ BibTex | Web page ]
[Bur07b]: E. Bursztein. Time has something to tell us about network address translation. In Proceedings of the 12th Nordic Workshop on Secure IT Systems (NordSec'07), Reykjavik, Iceland, October 2007.
[ BibTex | Web page | PDF ]
[JR07]: F. Jacquemard and M. Rusinowitch. Rewrite Closure of Hedge-Automata Languages. Research Report LSV-07-31, Laboratoire Spécification et Vérification, ENS Cachan, France, October 2007. 22 pages.
[ BibTex | Web page | PDF ]
[DLL07]: S. Delaune, H. Lin, and Ch. Lynch. Protocol verification via rigidashflexible resolution. In Proceedings of the 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'07), volume 4790 of Lecture Notes in Artificial Intelligence, pages 242--256, Yerevan, Armenia, October 2007. Springer.
doi: 10.1007/978-3-540-75560-9_19.
[ BibTex | DOI | Web page | PDF ]
[CD07]: V. Cortier and 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), volume 4790 of Lecture Notes in Artificial Intelligence, pages 196--210, Yerevan, Armenia, October 2007. Springer.
doi: 10.1007/978-3-540-75560-9_16.
[ BibTex | DOI | Web page | PS | PDF ]
[Laf07d]: P. Lafourcade. Rapport final d'activité à 11 mois, contrat CNRS/DGA référence : 06 60 019 00 470 75 01 << Utilisation et exploitation des théories équationnelles dans l'analyse des protocoles cryptographiques >>. Contract report, DGA, October 2007. 6 pages.
[ BibTex | Web page | PS ]
[Pro07]: A. ProNoBis. ProNoBis: Probability and Nondeterminism, Bisimulations and Security -- Rapport Final, October 2007.
[ BibTex | Web page | PDF ]
[GL07]: J. Goubault-Larrecq. Pronobis: Probability and nondeterminism, bisimulations and security. Rapport final ARC ProNoBis, October 2007.
[ BibTex ]
[Vac07]: C. Vacher. Accessibilité inverse dans les automates d'arbres à mémoire d'ordre supérieur. Rapport de Master, Master Parisien de Recherche en Informatique, Paris, France, September 2007.
[ BibTex | Web page | PDF ]
[CL07]: C. Cremers and P. Lafourcade. Comparing State Spaces in Automatic Security Protocol Verification. In Pre-proceedings of the 7th International Workshop on Automated Verification of Critical Systems (AVoCS'07), Oxford, UK, September 2007.
[ BibTex | Web page | PDF ]
[ACD07]: M. Arnaud, V. Cortier, and S. Delaune. Combining algorithms for deciding knowledge in security protocols. In Proceedings of the 6th International Symposium on Frontiers of Combining Systems (FroCoS'07), volume 4720 of Lecture Notes in Artificial Intelligence, pages 103--117, Liverpool, UK, September 2007. Springer.
doi: 10.1007/978-3-540-74621-8_7.
[ BibTex | DOI | Web page | PS | PDF ]
[KM07]: S. Kremer and L. Mazaré. Adaptive Soundness of Static Equivalence. In Proceedings of the 12th European Symposium on Research in Computer Security (ESORICS'07), volume 4734 of Lecture Notes in Computer Science, pages 610--625, Dresden, Germany, September 2007. Springer.
doi: 10.1007/978-3-540-74835-9_40.
[ BibTex | DOI | Web page | PDF ]
[Gou07c]: J. Goubault-Larrecq. Continuous Previsions. In Proceedings of the 16th Annual EACSL Conference on Computer Science Logic (CSL'07), volume 4646 of Lecture Notes in Computer Science, pages 542--557, Lausanne, Switzerland, September 2007. Springer.
doi: 10.1007/978-3-540-74915-8_40.
[ BibTex | DOI | Web page | PDF ]
[Laf07a]: P. Lafourcade. Intruder Deduction for the Equational Theory of phExclusive-or with Commutative and Distributive Encryption. In Proceedings of the 1st International Workshop on Security and Rewriting Techniques (SecReT'06), volume 171 of Electronic Notes in Theoretical Computer Science, pages 37--57, Venice, Italy, July 2007. Elsevier Science Publishers.
doi: 10.1016/j.entcs.2007.02.054.
[ BibTex | DOI | Web page | PS | PDF ]
[BJ07b]: A. Bouhoula and F. Jacquemard. Verifying Regular Trace Properties of Security Protocols with Explicit Destructors and Implicit Induction. In Proceedings of the Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (FCS-ARSPA'07), pages 27--44, Wroclaw, Poland, July 2007.
[ BibTex | Web page | PDF ]
[NT07]: M. Nesi and R. Treinen, editors. Preliminary Proceedings of the 2nd International Workshop on Security and Rewriting Techniques (SecReT'07), Paris, France, July 2007.
[ BibTex ]
[Gou07b]: J. Goubault-Larrecq. Continuous Capacities on Continuous State Spaces. In Proceedings of the 34th International Colloquium on Automata, Languages and Programming (ICALP'07), volume 4596 of Lecture Notes in Computer Science, pages 764--776, Wroclaw, Poland, July 2007. Springer.
doi: 10.1007/978-3-540-73420-8_66.
[ BibTex | DOI | Web page | PDF ]
[CDS07]: V. Cortier, S. Delaune, and G. Steel. A Formal Theory of Key Conjuring. In Proceedings of the 20th IEEE Computer Security Foundations Symposium (CSF'07), pages 79--93, Venice, Italy, July 2007. IEEE Computer Society Press.
doi: 10.1109/CSF.2007.5.
[ BibTex | DOI | Web page | PS | PDF ]
[Gou07d]: J. Goubault-Larrecq. On Noetherian Spaces. In Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science (LICS'07), pages 453--462, Wroclaw, Poland, July 2007. IEEE Computer Society Press.
doi: 10.1109/LICS.2007.34.
[ BibTex | DOI | Web page | PDF ]
[SC07]: G. Steel and J. Courant. A formal model for detecting parallel key search attacks. In Proceedings of the 3rd Workshop on Formal and Computational Cryptography (FCC'07), Venice, Italy, July 2007.
[ BibTex | Web page | PDF ]
[BCD07b]: S. Bursuc, H. Comon-Lundh, and S. Delaune. Deducibility Constraints, Equational Theory and Electronic Money. In Rewriting, Computation and Proof --- Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of his 60th Birthday, volume 4600 of Lecture Notes in Computer Science, pages 196--212, Cachan, France, June 2007. Springer.
doi: 10.1007/978-3-540-73147-4_10.
[ BibTex | DOI | Web page | PS ]
[CKK07]: H. Comon-Lundh, C. Kirchner, and H. Kirchner, editors. Rewriting, Computation and Proof --- Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of his 60th Birthday, volume 4600 of Lecture Notes in Computer Science, Cachan, France, June 2007. Springer.
doi: 10.1007/978-3-540-73147-4.
[ BibTex | DOI | Web page ]
[VG07]: K. N. Verma and J. Goubault-Larrecq. Alternating Two-Way AC-Tree Automata. Information and Computation, 205(6):817--869, June 2007.
doi: 10.1016/j.ic.2006.12.006.
[ BibTex | DOI | Web page | PS | PDF ]
[DK07]: S. Delaune and F. Klay. Synthèse des expérimentations. Technical Report 10, projet RNTL PROUVÉ, May 2007. 10 pages.
[ BibTex | Web page | PDF ]
[Bre07]: R. Bresciani. The ZRTP Protocol --- Security Considerations. Research Report LSV-07-20, Laboratoire Spécification et Vérification, ENS Cachan, France, May 2007. 23 pages.
[ BibTex | Web page | PS | PDF ]
[Laf07c]: P. Lafourcade. Rapport d'activités à 6 mois, contrat CNRS/DGA référence : 06 60 019 00 470 75 01 << Utilisation et exploitation des théories équationnelles dans l'analyse des protocoles cryptographiques >>. Contract report, DGA, April 2007. 5 pages.
[ BibTex | Web page | PS ]
[LLT07]: P. Lafourcade, D. Lugiez, and R. Treinen. Intruder Deduction for the Equational Theory of Abelian Groups with Distributive Encryption. Information and Computation, 205(4):581--623, April 2007.
doi: 10.1016/j.ic.2006.10.008.
[ BibTex | DOI | Web page | PS | PDF ]
[Maz07]: L. Mazaré. Computationally Sound Analysis of Protocols using Bilinear Pairings. In Preliminary Proceedings of the 7th International Workshop on Issues in the Theory of Security (WITS'07), pages 6--21, Braga, Portugal, March 2007.
[ BibTex | Web page | PDF ]
[CJP07]: H. Comon-Lundh, F. Jacquemard, and N. Perrin. Tree Automata with Memory, Visibility and Structural Constraints. In Proceedings of the 10th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'07), volume 4423 of Lecture Notes in Computer Science, pages 168--182, Braga, Portugal, March 2007. Springer.
doi: 10.1007/978-3-540-71389-0_13.
[ BibTex | DOI | Web page | PDF ]
[BJ07a]: A. Bouhoula and F. Jacquemard. Tree Automata, Implicit Induction and Explicit Destructors for Security Protocol Verification. Research Report LSV-07-10, Laboratoire Spécification et Vérification, ENS Cachan, France, February 2007. 21 pages.
[ BibTex | Web page | PDF ]
[KL07]: B. Ksieżopolski and P. Lafourcade. Attack and Revison of an Electronic Auction Protocol using OFMC. Technical Report 549, Department of Computer Science, ETH Zurich, Switzerland, February 2007. 13 pages.
[ BibTex | Web page | PDF ]
[BCD07a]: S. Bursuc, H. Comon-Lundh, and S. Delaune. Associative-Commutative Deducibility Constraints. In Proceedings of the 24th Annual Symposium on Theoretical Aspects of Computer Science (STACS'07), volume 4393 of Lecture Notes in Computer Science, pages 634--645, Aachen, Germany, February 2007. Springer.
doi: 10.1007/978-3-540-70918-3_54.
[ BibTex | DOI | Web page | PS | PDF ]
[Laf07b]: P. Lafourcade. Rapport d'activités à 3 mois, contrat CNRS/DGA référence : 06 60 019 00 470 75 01 << Utilisation et exploitation des théories équationnelles dans l'analyse des protocoles cryptographiques >>. Contract report, DGA, January 2007. 3 pages.
[ BibTex | Web page | PS ]
[Gou07a]: J. Goubault-Larrecq. Believe It Or Not, GOI is a Model of Classical Linear Logic. Research Report LSV-07-03, Laboratoire Spécification et Vérification, ENS Cachan, France, January 2007. 18 pages.
[ BibTex | Web page | PDF ]
[Bau07]: M. Baudet. Sécurité des protocoles cryptographiques : aspects logiques et calculatoires. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, January 2007.
[ BibTex | Web page | PS | PDF ]
[Com07]: H. Comon-Lundh. Soundness of abstract cryptography, 2007. Course notes (part 1), Symposium on Cryptography and Information Security (SCIS2008), Tokai, Japan.
[ BibTex | Web page | PDF ]
[Gou06]: J. Goubault-Larrecq. Preuve et vérification pour la sécurité et la sûreté. In Encyclopédie de l'informatique et des systèmes d'information, chapter I.6, pages 683--703. Vuibert, December 2006.
[ BibTex | Web page ]
[CKKW06]: V. Cortier, S. Kremer, R. Küsters, and B. 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), volume 4337 of Lecture Notes in Computer Science, pages 176--187, Kolkata, India, December 2006. Springer.
doi: 10.1007/11944836_18.
[ BibTex | DOI | Web page | PS | PDF ]
[Del06b]: S. Delaune. An Undecidability Result for AGh. Theoretical Computer Science, 368(1-2):161--167, December 2006.
doi: 10.1016/j.tcs.2006.08.018.
[ BibTex | DOI | Web page | PS | PDF ]
[KBL⁺06]: F. Klay, L. Bozga, Y. Lakhnech, L. Mazaré, S. Delaune, and S. Kremer. Retour d'expérience sur la validation du vote électronique. Technical Report 9, projet RNTL PROUVÉ, November 2006. 47 pages.
[ BibTex | Web page | PDF ]
[MBDC⁺06]: F. Mancinelli, J. Boender, R. Di Cosmo, J. Vouillon, B. Durak, X. Leroy, and R. Treinen. Managing the Complexity of Large Free and Open Source Package-Based Software Distributions. In Proceedings of the 21st IEEE/ACM International Conference on Automated Software Engineering (ASE'06), pages 199--208, Tokyo, Japan, September 2006. IEEE Computer Society Press.
doi: 10.1109/ASE.2006.49.
[ BibTex | DOI | Web page | PDF ]
[MOJ06]: I. Mitsuhashi, M. Oyamaguchi, and F. Jacquemard. The Confluence Problem for Flat TRSs. In Proceedings of the 8th International Conference on Artificial Intelligence and Symbolic Computation (AISC'06), volume 4120 of Lecture Notes in Artificial Intelligence, pages 68--81, Beijing, China, September 2006. Springer.
doi: 10.1007/11856290_8.
[ BibTex | DOI | Web page | PDF ]
[Laf06]: P. Lafourcade. Vérification des protocoles cryptographiques en présence de théories équationnelles. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, September 2006. 209 pages.
[ BibTex | Web page | PS | PDF ]
[Bur06]: S. Bursuc. Contraintes de déductibilité modulo Associativité-Commutativité. Rapport de Master, Master Parisien de Recherche en Informatique, Paris, France, September 2006.
[ BibTex | Web page | PDF ]
[JRV06]: F. Jacquemard, M. Rusinowitch, and L. Vigneron. Tree automata with equality constraints modulo equational theories. In Proceedings of the 3rd International Joint Conference on Automated Reasoning (IJCAR'06), volume 4130 of Lecture Notes in Artificial Intelligence, pages 557--571, Seattle, Washington, USA, August 2006. Springer-Verlag.
doi: 10.1007/11814771_45.
[ BibTex | DOI | Web page ]
[LLT06]: P. Lafourcade, D. Lugiez, and R. Treinen. ACUNh: Unification and Disunification Using Automata Theory. In Proceedings of the 20th International Workshop on Unification (UNIF'06), pages 6--20, Seattle, Washington, USA, August 2006.
[ BibTex | Web page | PS | PDF ]
[BJ06a]: A. Bouhoula and F. Jacquemard. Automating Sufficient Completeness Check for Conditional and Constrained TRS. In Proceedings of the 20th International Workshop on Unification (UNIF'06), Seattle, Washington, USA, August 2006.
[ BibTex | Web page | PDF ]
[BJ06b]: A. Bouhoula and F. Jacquemard. Security Protocols Verification with Implicit Induction and Explicit Destructors. In Preliminary Proceedings of the 1st International Workshop on Security and Rewriting Techniques (SecReT'06), pages 37--44, Venice, Italy, July 2006.
[ BibTex | Web page | PDF ]
[DKR06a]: S. Delaune, S. Kremer, and M. D. Ryan. Coercion-Resistance and Receipt-Freeness in Electronic Voting. In Proceedings of the 19th IEEE Computer Security Foundations Workshop (CSFW'06), pages 28--39, Venice, Italy, July 2006. IEEE Computer Society Press.
doi: 10.1109/CSFW.2006.8.
[ BibTex | DOI | Web page | PS | PDF ]
[DLLT06]: S. Delaune, P. Lafourcade, D. Lugiez, and R. Treinen. Symbolic Protocol Analysis in Presence of a Homomorphism Operator and phExclusive Or. In Proceedings of the 33rd International Colloquium on Automata, Languages and Programming (ICALP'06) --- Part II, volume 4052 of Lecture Notes in Computer Science, pages 132--143, Venice, Italy, July 2006. Springer.
doi: 10.1007/11787006_12.
[ BibTex | DOI | Web page | PS | PDF ]
[CK06]: V. Cortier and S. Kremer, editors. Proceedings of the 2nd Workshop on Formal and Computational Cryptography (FCC'06), Venice, Italy, July 2006.
[ BibTex | Web page ]
[DKR06b]: S. Delaune, S. Kremer, and M. D. Ryan. Verifying Properties of Electronic Voting Protocols. In Proceedings of the IAVoSS Workshop On Trustworthy Elections (WOTE'06), pages 45--52, Cambridge, UK, June 2006.
[ BibTex | Web page | PS | PDF ]
[Ber06]: V. Bernat. Théories de l'intrus pour la vérification des protocoles cryptographiques. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, June 2006.
[ BibTex | Web page | PS | PDF ]
[Del06c]: S. Delaune. Vérification des protocoles cryptographiques et propriétés algébriques. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, June 2006.
[ BibTex | Web page | PS | PDF ]
[OG06]: J. Olivain and J. Goubault-Larrecq. Detecting Subverted Cryptographic Protocols by Entropy Checking. Research Report LSV-06-13, Laboratoire Spécification et Vérification, ENS Cachan, France, June 2006. 19 pages.
[ BibTex | Web page | PDF ]
[BDCD⁺06]: J. Boender, R. Di Cosmo, B. Durak, X. Leroy, F. Mancinelli, M. Morgado, D. Pinheiro, R. Treinen, P. Trezentos, and J. Vouillon. News from the EDOS project: improving the maintenance of free software distributions. In Proceedings of the International Workshop on Free Software (IWFS'06), pages 199--207, Porto Allegre, Brazil, April 2006.
[ BibTex | Web page | PDF ]
[ABW06]: M. Abadi, M. Baudet, and B. Warinschi. Guessing Attacks and the Computational Soundness of Static Equivalence. In Proceedings of the 9th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'06), volume 3921 of Lecture Notes in Computer Science, pages 398--412, Vienna, Austria, March 2006. Springer.
doi: 10.1007/11690634_27.
[ BibTex | DOI | Web page | PS | PDF ]
[Del06a]: S. Delaune. Easy Intruder Deduction Problems with Homomorphisms. Information Processing Letters, 97(6):213--218, March 2006.
doi: 10.1016/j.ipl.2005.11.008.
[ BibTex | DOI | Web page | PS | PDF ]
[CDL06]: V. Cortier, S. Delaune, and P. Lafourcade. A Survey of Algebraic Properties Used in Cryptographic Protocols. Journal of Computer Security, 14(1):1--43, 2006.
[ BibTex | Web page | PS | PDF ]
[CKS06]: R. Chadha, S. Kremer, and A. Scedrov. Formal Analysis of Multi-Party Contract Signing. Journal of Automated Reasoning, 36(1-2):39--83, January 2006.
doi: 10.1007/s10817-005-9019-5.
[ BibTex | DOI | Web page | PDF ]
[DJ06]: S. Delaune and F. Jacquemard. Decision Procedures for the Security of Protocols with Probabilistic Encryption against Offline Dictionary Attacks. Journal of Automated Reasoning, 36(1-2):85--124, January 2006.
doi: 10.1007/s10817-005-9017-7.
[ BibTex | DOI | Web page | PS ]
[Bau06]: M. Baudet. Random Polynomial-Time Attacks and Dolev-Yao Models. Journal of Automata, Languages and Combinatorics, 11(1):7--21, 2006.
[ BibTex | Web page | PS | PDF ]

This file was generated by bibtex2html 1.98.

Publications : SECSI

About LSV