Publications

2021

  • M. Barbosa, G. Barthe, K. Bhargavan, B. Blanchet, C. Cremers, K. Liao, and B. Parno, “Sok: computer-aided cryptography,” in Ieee symposium on security and privacy (s&p’21), 2021.
    [Bibtex]
    @inproceedings{BarbosaetalOakland21,
    author = {Manuel Barbosa and
    Gilles Barthe and
    Karthikeyan Bhargavan and
    Bruno Blanchet and
    Cas Cremers and
    Kevin Liao and
    Bryan Parno},
    title = {SoK: Computer-Aided Cryptography},
    booktitle = {IEEE Symposium on Security and Privacy (S\&P'21)},
    year = {2021},
    optpages = {},
    optmonth = {},
    optaddress = {},
    publisher = {IEEE Computer Society},
    url = {https://bblanche.gitlabpages.inria.fr/publications/BarbosaetalOakland21.pdf}
    }
  • A. Koutsos, “Decidability of a sound set of inference rules for computational indistinguishability,” ACM trans. comput. log., vol. 22, iss. 1, p. 3:1–3:44, 2021.
    [Bibtex]
    @article{DBLP:journals/tocl/Koutsos21,
    author = {Adrien Koutsos},
    title = {Decidability of a Sound Set of Inference Rules for Computational Indistinguishability},
    journal = {{ACM} Trans. Comput. Log.},
    volume = {22},
    number = {1},
    pages = {3:1--3:44},
    year = {2021}
    }

2020

  • J. Alwen, B. Blanchet, E. Hauck, E. Kiltz, B. Lipp, and D. Riepel, Analysing the HPKE standard, 2020.
    [Bibtex]
    @misc{cryptoeprint:2020:1499,
    author = {Joël Alwen and Bruno Blanchet and Eduard Hauck and Eike Kiltz and Benjamin Lipp and Doreen Riepel},
    title = {Analysing the {HPKE} Standard},
    howpublished = {Cryptology ePrint Archive, Report 2020/1499},
    year = {2020},
    month = nov,
    url = {https://eprint.iacr.org/2020/1499}
    }
  • K. Maillard, C. Hritcu, E. Rivas, and A. Van Muylder, The next 700 relational program logics, 2020.
    [Bibtex]
    @misc{relational700,
    author = {Kenji Maillard and
    Catalin Hritcu and
    Exequiel Rivas and
    Antoine {Van Muylder}},
    title = {The Next 700 Relational Program Logics},
    howpublished = {To appear at POPL},
    year = {2020},
    url = {https://arxiv.org/abs/1907.05244}
    }
  • [DOI] M. Polubelova, K. Bhargavan, J. Protzenko, B. Beurdouche, A. Fromherz, N. Kulatova, and S. Z. Béguelin, “Haclxn: verified generic SIMD crypto (for all your favourite platforms),” in CCS ’20: 2020 ACM SIGSAC conference on computer and communications security, virtual event, usa, november 9-13, 2020, 2020, p. 899–918.
    [Bibtex]
    @inproceedings{DBLP:conf/ccs/PolubelovaBPBFK20,
    author = {Marina Polubelova and
    Karthikeyan Bhargavan and
    Jonathan Protzenko and
    Benjamin Beurdouche and
    Aymeric Fromherz and
    Natalia Kulatova and
    Santiago Zanella B{\'{e}}guelin},
    editor = {Jay Ligatti and
    Xinming Ou and
    Jonathan Katz and
    Giovanni Vigna},
    title = {HACLxN: Verified Generic {SIMD} Crypto (for all your favourite platforms)},
    booktitle = {{CCS} '20: 2020 {ACM} {SIGSAC} Conference on Computer and Communications
    Security, Virtual Event, USA, November 9-13, 2020},
    pages = {899--918},
    publisher = {{ACM}},
    year = {2020},
    url = {https://doi.org/10.1145/3372297.3423352},
    doi = {10.1145/3372297.3423352},
    timestamp = {Tue, 10 Nov 2020 20:00:39 +0100},
    biburl = {https://dblp.org/rec/conf/ccs/PolubelovaBPBFK20.bib},
    bibsource = {dblp computer science bibliography, https://dblp.org}
    }
  • [DOI] J. Protzenko, B. Parno, A. Fromherz, C. Hawblitzel, M. Polubelova, K. Bhargavan, B. Beurdouche, J. Choi, A. D. -, C. Fournet, N. Kulatova, T. Ramananandro, A. Rastogi, N. Swamy, C. M. Wintersteiger, and S. Z. Béguelin, “Evercrypt: A fast, verified, cross-platform cryptographic provider,” in 2020 IEEE symposium on security and privacy, SP 2020, san francisco, ca, usa, may 18-21, 2020, 2020, p. 983–1002.
    [Bibtex]
    @inproceedings{DBLP:conf/sp/ProtzenkoPFHPBB20,
    author = {Jonathan Protzenko and
    Bryan Parno and
    Aymeric Fromherz and
    Chris Hawblitzel and
    Marina Polubelova and
    Karthikeyan Bhargavan and
    Benjamin Beurdouche and
    Joonwon Choi and
    Antoine Delignat{-}Lavaud and
    C{\'{e}}dric Fournet and
    Natalia Kulatova and
    Tahina Ramananandro and
    Aseem Rastogi and
    Nikhil Swamy and
    Christoph M. Wintersteiger and
    Santiago Zanella B{\'{e}}guelin},
    title = {EverCrypt: {A} Fast, Verified, Cross-Platform Cryptographic Provider},
    booktitle = {2020 {IEEE} Symposium on Security and Privacy, {SP} 2020, San Francisco,
    CA, USA, May 18-21, 2020},
    pages = {983--1002},
    publisher = {{IEEE}},
    year = {2020},
    url = {https://doi.org/10.1109/SP40000.2020.00114},
    doi = {10.1109/SP40000.2020.00114},
    timestamp = {Sun, 25 Oct 2020 22:57:11 +0100},
    biburl = {https://dblp.org/rec/conf/sp/ProtzenkoPFHPBB20.bib},
    bibsource = {dblp computer science bibliography, https://dblp.org}
    }
  • [DOI] Progress in cryptology – INDOCRYPT 2020 – 21st international conference on cryptology in india, bangalore, india, december 13-16, 2020, proceedingsSpringer, 2020.
    [Bibtex]
    @proceedings{DBLP:conf/indocrypt/2020,
    editor = {Karthikeyan Bhargavan and
    Elisabeth Oswald and
    Manoj Prabhakaran},
    title = {Progress in Cryptology - {INDOCRYPT} 2020 - 21st International Conference
    on Cryptology in India, Bangalore, India, December 13-16, 2020, Proceedings},
    series = {Lecture Notes in Computer Science},
    volume = {12578},
    publisher = {Springer},
    year = {2020},
    url = {https://doi.org/10.1007/978-3-030-65277-7},
    doi = {10.1007/978-3-030-65277-7},
    isbn = {978-3-030-65276-0},
    timestamp = {Wed, 09 Dec 2020 15:35:12 +0100},
    biburl = {https://dblp.org/rec/conf/indocrypt/2020.bib},
    bibsource = {dblp computer science bibliography, https://dblp.org}
    }

2019

  • T. Ramananandro, A. D. -, C. Fournet, N. Swamy, T. Chajed, N. Kobeissi, and J. Protzenko, “Everparse: verified secure zero-copy parsers for authenticated message formats,” in 28th USENIX security symposium, USENIX security 2019, santa clara, ca, usa, august 14-16, 2019, 2019, p. 1465–1482.
    [Bibtex]
    @inproceedings{RamananandroDFS19,
    author = {Tahina Ramananandro and
    Antoine Delignat{-}Lavaud and
    C{\'{e}}dric Fournet and
    Nikhil Swamy and
    Tej Chajed and
    Nadim Kobeissi and
    Jonathan Protzenko},
    editor = {Nadia Heninger and
    Patrick Traynor},
    title = {EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message
    Formats},
    booktitle = {28th {USENIX} Security Symposium, {USENIX} Security 2019, Santa Clara,
    CA, USA, August 14-16, 2019},
    pages = {1465--1482},
    publisher = {{USENIX} Association},
    year = {2019},
    url = {https://www.usenix.org/conference/usenixsecurity19/presentation/delignat-lavaud},
    timestamp = {Tue, 03 Sep 2019 16:39:56 +0200},
    biburl = {https://dblp.org/rec/bib/conf/uss/RamananandroDFS19},
    bibsource = {dblp computer science bibliography, https://dblp.org}
    }
  • [PDF] [DOI] R. Blanco, D. Miller, and A. Momigliano, “Property-Based Testing via Proof Reconstruction,” in PPDP 2019 – 21st International Symposium on Principles and Practice of Programming Languages, Porto, Portugal, 2019, pp. 1-13.
    [Bibtex]
    @inproceedings{blanco:hal-02368931,
    title = {{Property-Based Testing via Proof Reconstruction}},
    author = {Blanco, Roberto and Miller, Dale and Momigliano, Alberto},
    url = {https://hal.inria.fr/hal-02368931},
    booktitle = {{PPDP 2019 - 21st International Symposium on Principles and Practice of Programming Languages}},
    address = {Porto, Portugal},
    publisher = {{ACM Press}},
    pages = {1-13},
    year = {2019},
    month = Oct,
    doi = {10.1145/3354166.3354170},
    keywords = {Logic and verification ; Software and its engineering ; Theory of computation ; Proof theory ; Formal software verification},
    pdf = {https://hal.inria.fr/hal-02368931/file/ppdp2019-pbt.pdf},
    hal_id = {hal-02368931},
    hal_version = {v1}
    }
  • [PDF] E. Rivas and M. Jaskelioff, Monads with merging, 2019.
    [Bibtex]
    @unpublished{rivas:hal-02150199,
    title = {{Monads with merging}},
    author = {Rivas, Exequiel and Jaskelioff, Mauro},
    url = {https://hal.inria.fr/hal-02150199},
    note = {preprint},
    year = {2019},
    month = Jun,
    keywords = {Concurrency ; Process Algebra ; Bimonoids ; Monads},
    pdf = {https://hal.inria.fr/hal-02150199/file/main.pdf},
    hal_id = {hal-02150199},
    hal_version = {v1}
    }
  • [DOI] R. Cruz and É. Tanter, “Polymorphic relaxed noninterference,” in Proceedings of the IEEE secure development conference (secdev 2019), McLean, VA, USA, 2019, p. 101–113.
    [Bibtex]
    @inproceedings{cruzTanter:secdev2019,
    author = {Raimil Cruz and {\'E}ric Tanter},
    title = {Polymorphic Relaxed Noninterference},
    booktitle = {Proceedings of the {IEEE} Secure Development Conference (SecDev 2019)},
    year = 2019,
    month = sep,
    address = {McLean, VA, USA},
    publisher = {IEEE Computer Society Press},
    pages = {101--113},
    url = {http://pleiad.dcc.uchile.cl/papers/2019/cruzTanter-secdev2019.pdf},
    doi = {10.1109/SecDev.2019.00021}
    }
  • [DOI] P. Pédrot, N. Tabareau, H. Fehrmann, and É. Tanter, “A reasonably exceptional type theory,” Proceedings of the acm on programming languages, vol. 3, iss. ICFP, p. 108:1–108:29, 2019.
    [Bibtex]
    @article{pedrotAl:icfp2019,
    author = {Pierre-Marie P{\'e}drot and Nicolas Tabareau and Hans Fehrmann and {\'E}ric Tanter},
    title = {A Reasonably Exceptional Type Theory},
    pages = {108:1--108:29},
    url = {http://pleiad.dcc.uchile.cl/papers/2019/pedrotAl-icfp2019.pdf},
    doi = {10.1145/3341712},
    journal = {Proceedings of the ACM on Programming Languages},
    volume = 3,
    number = {ICFP},
    month = aug,
    year = 2019,
    publisher = {ACM Press}
    }
  • [DOI] J. Eremondi, É. Tanter, and R. Garcia, “Approximate normalization for gradual dependent types,” Proceedings of the acm on programming languages, vol. 3, iss. ICFP, p. 88:1–88:30, 2019.
    [Bibtex]
    @article{eremondiAl:icfp2019,
    author = {Joseph Eremondi and {\'E}ric Tanter and Ronald Garcia},
    title = {Approximate Normalization for Gradual Dependent Types},
    pages = {88:1--88:30},
    url = {http://pleiad.dcc.uchile.cl/papers/2019/eremondiAl-icfp2019.pdf},
    doi = {10.1145/3341692},
    journal = {Proceedings of the ACM on Programming Languages},
    volume = 3,
    number = {ICFP},
    month = aug,
    year = 2019,
    publisher = {ACM Press}
    }
  • [DOI] M. Toro, E. Labrada, and É. Tanter, “Gradual parametricity, revisited,” Proceedings of the acm on programming languages, vol. 3, iss. POPL, p. 17:1–17:30, 2019.
    [Bibtex]
    @article{toroAl:popl2019,
    author = {Mat{\'i}as Toro and Elizabeth Labrada and {\'E}ric Tanter},
    title = {Gradual Parametricity, Revisited},
    pages = {17:1--17:30},
    url = {http://pleiad.dcc.uchile.cl/papers/2019/toroAl-popl2019.pdf},
    doi = {10.1145/3290330},
    journal = {Proceedings of the ACM on Programming Languages},
    volume = 3,
    number = {POPL},
    month = jan,
    year = 2019,
    publisher = {ACM Press}
    }
  • [DOI] K. Maillard, D. Ahman, R. Atkey, G. Martínez, C. Hritcu, E. Rivas, and É. Tanter, “Dijkstra monads for all,” PACMPL, vol. 3, iss. {ICFP}, p. 104:1–104:29, 2019.
    [Bibtex]
    @article{dm4all,
    author = {Kenji Maillard and
    Danel Ahman and
    Robert Atkey and
    Guido Mart{\'{\i}}nez and
    Catalin Hritcu and
    Exequiel Rivas and
    {\'{E}}ric Tanter},
    title = {Dijkstra Monads for All},
    journal = {{PACMPL}},
    volume = {3},
    number = {{ICFP}},
    pages = {104:1--104:29},
    year = {2019},
    ee = {https://doi.org/10.1145/3341708},
    doi = {10.1145/3341708},
    url = {https://arxiv.org/abs/1903.01237}
    }
  • C. Hritcu, “The quest for formally secure compartmentalizing compilation,” Habilitation thesis PhD Thesis, 2019.
    [Bibtex]
    @phdthesis{Hritcu:19,
    author = {Catalin Hritcu},
    title = {The Quest for Formally Secure Compartmentalizing Compilation},
    school = {ENS Paris; PSL Research University},
    year = {2019},
    month = jan,
    type = {Habilitation thesis},
    url = {http://prosecco.gforge.inria.fr/personal/hritcu/publications/catalin_habil.pdf},
    key = {Theses}
    }
  • B. Lipp, B. Blanchet, and K. Bhargavan, “A mechanised cryptographic proof of the WireGuard virtual private network protocol,” in Ieee european symposium on security and privacy (euros&p’19), Stockholm, Sweden, 2019, p. 231–246.
    [Bibtex]
    @inproceedings{LippBlanchetBharagavanEuroSP19,
    author = {Benjamin Lipp and Bruno Blanchet and Karthikeyan Bhargavan},
    title = {A Mechanised Cryptographic Proof of the
    {W}ire{G}uard Virtual Private Network Protocol},
    booktitle = {IEEE European Symposium on Security and Privacy (EuroS\&P'19)},
    year = 2019,
    pages = {231--246},
    month = jun,
    address = {Stockholm, Sweden},
    publisher = {IEEE Computer Society},
    url = {https://hal.inria.fr/hal-02100345/document}
    }
  • B. Lipp, B. Blanchet, and K. Bhargavan, “A mechanised cryptographic proof of the WireGuard virtual private network protocol,” Inria, Research report 9269, 2019.
    [Bibtex]
    @techreport{RR-9269,
    author = {Benjamin Lipp and Bruno Blanchet and Karthikeyan Bhargavan},
    title = {A Mechanised Cryptographic Proof of the
    {W}ire{G}uard Virtual Private Network Protocol},
    institution = {Inria},
    year = 2019,
    type = {Research report},
    number = 9269,
    month = apr,
    url = {https://hal.inria.fr/hal-02100345}
    }
  • N. Kobeissi, G. Nicolas, and K. Bhargavan, “Noise Explorer: Fully automated modeling and verification for arbitrary Noise protocols,” in Ieee european symposium on security and privacy (euros&p 2019), Stockholm, Sweden, 2019.
    [Bibtex]
    @inproceedings{KobeissiNicolasBhargavanEuroSP19,
    author = {Nadim Kobeissi and Georgio Nicolas and Karthikeyan Bhargavan},
    title = {{Noise} {Explorer}: {Fully} Automated Modeling and Verification for Arbitrary {Noise} Protocols},
    booktitle = {IEEE European Symposium on Security and Privacy (EuroS\&P 2019)},
    year = 2019,
    month = jun,
    address = {Stockholm, Sweden},
    publisher = {IEEE Computer Society},
    url = {https://eprint.iacr.org/2018/766},
    note = {To appear.
    The tool is available at \url{https://noiseexplorer.com/}}
    }
  • [DOI] C. Abate, R. Blanco, D. Garg, C. Hritcu, M. Patrignani, and J. Thibault, “Journey beyond full abstraction: exploring robust property preservation for secure compilation,” in 32nd ieee computer security foundations symposium (csf), 2019, pp. 256-271.
    [Bibtex]
    @inproceedings{AbateBGHPT19,
    author = {Carmine Abate and
    Roberto Blanco and
    Deepak Garg and
    Catalin Hritcu and
    Marco Patrignani and
    J\'er\'emy Thibault},
    title = {Journey Beyond Full Abstraction:
    Exploring Robust Property Preservation for Secure Compilation},
    booktitle = {32nd IEEE Computer Security Foundations Symposium (CSF)},
    shortbooktitle = {CSF},
    pages = {256-271},
    publisher = {IEEE},
    ee = {https://doi.org/10.1109/CSF.2019.00025},
    doi = {10.1109/CSF.2019.00025},
    url = {https://arxiv.org/abs/1807.04603},
    month = jun,
    year = 2019
    }
  • [DOI] G. Martínez, D. Ahman, V. Dumitrescu, N. Giannarakis, C. Hawblitzel, C. Hritcu, M. Narasimhamurthy, Z. Paraskevopoulou, C. Pit-Claudel, J. Protzenko, T. Ramananandro, A. Rastogi, and N. Swamy, “Meta-F*: proof automation with SMT, tactics, and metaprograms,” in 28th european symposium on programming (esop), 2019, p. 30–59.
    [Bibtex]
    @inproceedings{metafstar,
    author = {Guido Mart\'inez and
    Danel Ahman and
    Victor Dumitrescu and
    Nick Giannarakis and
    Chris Hawblitzel and
    Catalin Hritcu and
    Monal Narasimhamurthy and
    Zoe Paraskevopoulou and
    Cl\'ement Pit-Claudel and
    Jonathan Protzenko and
    Tahina Ramananandro and
    Aseem Rastogi and
    Nikhil Swamy},
    title = {{Meta-F*}: Proof Automation with {SMT}, Tactics, and Metaprograms},
    booktitle = {28th European Symposium on Programming (ESOP)},
    shortbooktitle = {ESOP},
    pages = {30--59},
    publisher = {Springer},
    year = {2019},
    month = april,
    url = {https://fstar-lang.org/papers/metafstar},
    ee = {https://doi.org/10.1007/978-3-030-17184-1\_2},
    doi = {10.1007/978-3-030-17184-1\_2}
    }
  • J. Protzenko, B. Beurdouche, D. Merigoux, and K. Bhargavan, “Formally Verified Cryptographic Web Applications in WebAssembly,” in IEEE Symposium on Security and Privacy (S&P), 2019.
    [Bibtex]
    @inproceedings{signal-wasm,
    author = {Jonathan Protzenko and Benjamin Beurdouche and Denis Merigoux and Karthikeyan Bhargavan},
    title = {{Formally Verified Cryptographic Web Applications in WebAssembly}},
    booktitle = {{IEEE Symposium on Security and Privacy (S\&P)}},
    url = {https://eprint.iacr.org/2019/542},
    year = {2019}
    }
  • D. Adrian, K. Bhargavan, Z. Durumeric, P. Gaudry, M. Green, A. J. Halderman, N. Heninger, D. Springall, E. Thomé, L. Valenta, B. VanderSloot, E. Wustrow, S. Z. -, and P. Zimmermann, “Imperfect forward secrecy: how diffie-hellman fails in practice,” Communications of the ACM, vol. 62, iss. 1, p. 106–114, 2019.
    [Bibtex]
    @article{DBLP:journals/cacm/AdrianBDGGHHSTV19,
    author = {David Adrian and Karthikeyan Bhargavan and Zakir Durumeric
    and Pierrick Gaudry and Matthew Green and
    J. Alex Halderman and Nadia Heninger and Drew Springall
    and Emmanuel Thom{\'{e}} and Luke Valenta and
    Benjamin VanderSloot and
    Eric Wustrow and
    Santiago Zanella{-}B{\'{e}}guelin and
    Paul Zimmermann},
    title = {Imperfect forward secrecy: how Diffie-Hellman fails
    in practice},
    journal = {Communications of the {ACM}},
    volume = {62},
    number = {1},
    pages = {106--114},
    year = {2019}
    }
  • [DOI] K. Bhargavan and P. Naldurg, “Practical Formal Methods for Real World Cryptography (Invited Talk),” in 39th iarcs annual conference on foundations of software technology and theoretical computer science (fsttcs 2019), Dagstuhl, Germany, 2019, p. 1:1–1:12.
    [Bibtex]
    @inproceedings{bhargavan_et_al:LIPIcs:2019:11563,
    author = {Karthikeyan Bhargavan and Prasad Naldurg},
    title = {{Practical Formal Methods for Real World Cryptography (Invited Talk)}},
    booktitle = {39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)},
    pages = {1:1--1:12},
    series = {Leibniz International Proceedings in Informatics (LIPIcs)},
    isbn = {978-3-95977-131-3},
    issn = {1868-8969},
    year = {2019},
    volume = {150},
    editor = {Arkadev Chattopadhyay and Paul Gastin},
    publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
    address = {Dagstuhl, Germany},
    url = {http://drops.dagstuhl.de/opus/volltexte/2019/11563},
    urn = {urn:nbn:de:0030-drops-115632},
    doi = {10.4230/LIPIcs.FSTTCS.2019.1},
    annote = {Keywords: Formal verification, Applied cryptography, Security protocols, Machine learning}
    }

2018

  • B. Blanchet, “Composition theorems for CryptoVerif and application to TLS 1.3,” in 31st ieee computer security foundations symposium (csf’18), Oxford, UK, 2018, p. 16–30.
    [Bibtex]
    @inproceedings{BlanchetCSF18,
    author = {Bruno Blanchet},
    title = {Composition Theorems for {C}rypto{V}erif and Application to {TLS} 1.3},
    booktitle = {31st IEEE Computer Security Foundations Symposium (CSF'18)},
    year = {2018},
    pages = {16--30},
    month = jul,
    address = {Oxford, UK},
    publisher = {IEEE Computer Society},
    url = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetCSF18.html}
    }
  • B. Blanchet, “Composition theorems for CryptoVerif and application to TLS~1.3,” Inria, Research Report RR-9171, 2018.
    [Bibtex]
    @techreport{BlanchetInria18,
    author = {Bruno Blanchet},
    title = {Composition Theorems for {C}rypto{V}erif and Application to {TLS}~1.3},
    institution = {Inria},
    year = 2018,
    type = {Research Report},
    number = {RR-9171},
    month = apr,
    url = {https://hal.inria.fr/hal-01764527}
    }
  • B. Blanchet and B. Smyth, “Automated reasoning for equivalences in the applied pi calculus with barriers,” Journal of computer security, vol. 26, iss. 3, p. 367–422, 2018.
    [Bibtex]
    @article{BlanchetSmythJCS18,
    author = {Bruno Blanchet and Ben Smyth},
    title = {Automated reasoning for equivalences in the applied pi calculus with barriers},
    journal = {Journal of Computer Security},
    year = 2018,
    volume = 26,
    number = 3,
    pages = {367--422},
    url = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetSmythJCS18.html}
    }
  • [PDF] [DOI] I. B. Guirat and H. Halpin, “Formal verification of the W3C Web Authentication Protocol,” Proceedings of the 5th Annual Symposium and Bootcamp on Hot Topics in the Science of Security – HoTSoS ’18, pp. 1-10, 2018.
    [Bibtex]
    @article{guirat:hal-01966563,
    title = {{Formal verification of the W3C Web Authentication Protocol}},
    author = {Guirat, Iness Ben and Halpin, Harry},
    url = {https://hal.inria.fr/hal-01966563},
    journal = {{Proceedings of the 5th Annual Symposium and Bootcamp on Hot Topics in the Science of Security - HoTSoS '18}},
    pages = {1-10},
    year = {2018},
    doi = {10.1145/3190619.3190640},
    pdf = {https://hal.inria.fr/hal-01966563/file/main.pdf},
    hal_id = {hal-01966563},
    hal_version = {v1}
    }
  • [PDF] H. Halpin, Decentralizing the Social Web, 2018.
    [Bibtex]
    @misc{halpin:hal-01966561,
    title = {{Decentralizing the Social Web}},
    author = {Halpin, Harry},
    url = {https://hal.inria.fr/hal-01966561},
    howpublished = {{Internet Science 2018}},
    year = {2018},
    month = Oct,
    keywords = {standards ; social web ; decentralization ; blockchain},
    pdf = {https://hal.inria.fr/hal-01966561/file/main.pdf},
    hal_id = {hal-01966561},
    hal_version = {v1}
    }
  • [PDF] H. Halpin, K. Ermoshina, and F. Musiani, Co-ordinating Developers and High-Risk Users of Privacy-Enhanced Secure Messaging Protocols, 2018.
    [Bibtex]
    @misc{halpin:hal-01966560,
    title = {{Co-ordinating Developers and High-Risk Users of Privacy-Enhanced Secure Messaging Protocols}},
    author = {Halpin, Harry and Ermoshina, Ksenia and Musiani, Francesca},
    url = {https://hal.inria.fr/hal-01966560},
    howpublished = {{Security Standardisation Research Conference}},
    year = {2018},
    month = Nov,
    pdf = {https://hal.inria.fr/hal-01966560/file/main.pdf},
    hal_id = {hal-01966560},
    hal_version = {v1}
    }
  • [DOI] N. Tabareau, É. Tanter, and M. Sozeau, “Equivalences for free: univalent parametricity for effective transport,” PACMPL, vol. 2, iss. {ICFP}, p. 92:1–92:29, 2018.
    [Bibtex]
    @article{DBLP:journals/pacmpl/TabareauTS18,
    author = {Nicolas Tabareau and
    {\'{E}}ric Tanter and
    Matthieu Sozeau},
    title = {Equivalences for free: univalent parametricity for effective transport},
    journal = {{PACMPL}},
    volume = {2},
    number = {{ICFP}},
    pages = {92:1--92:29},
    year = {2018},
    ee = {https://doi.org/10.1145/3236787},
    doi = {10.1145/3236787},
    timestamp = {Wed, 21 Nov 2018 12:44:28 +0100},
    biburl = {https://dblp.org/rec/bib/journals/pacmpl/TabareauTS18},
    bibsource = {dblp computer science bibliography, https://dblp.org},
    url = {https://hal.inria.fr/hal-01559073}
    }
  • [DOI] N. Vazou, É. Tanter, and D. V. Horn, “Gradual liquid type inference,” PACMPL, vol. 2, iss. {OOPSLA}, p. 132:1–132:25, 2018.
    [Bibtex]
    @article{DBLP:journals/pacmpl/VazouTH18,
    author = {Niki Vazou and
    {\'{E}}ric Tanter and
    David Van Horn},
    title = {Gradual liquid type inference},
    journal = {{PACMPL}},
    volume = {2},
    number = {{OOPSLA}},
    pages = {132:1--132:25},
    year = {2018},
    ee = {https://doi.org/10.1145/3276502},
    doi = {10.1145/3276502},
    timestamp = {Wed, 21 Nov 2018 12:44:28 +0100},
    biburl = {https://dblp.org/rec/bib/journals/pacmpl/VazouTH18},
    bibsource = {dblp computer science bibliography, https://dblp.org},
    url = {https://arxiv.org/abs/1807.02132}
    }
  • M. Toro, R. Garcia, and É. Tanter, “Type-driven gradual security with references,” Acm transactions on programming languages and systems, vol. 40, iss. 4, 2018.
    [Bibtex]
    @article{toroAl:toplas2018,
    author = {Mat{\'i}as Toro and Ronald Garcia and {\'E}ric Tanter},
    title = {Type-Driven Gradual Security with References},
    journal = {ACM Transactions on Programming Languages and Systems},
    publisher = {ACM Press},
    volume = 40,
    number = 4,
    year = 2018,
    url = {http://pleiad.dcc.uchile.cl/papers/2018/toroAl-toplas2018.pdf},
    webnote = {To be presented at POPL 2019}
    }
  • M. Toro, E. Labrada, and É. Tanter, “Gradual parametricity, revisited,” Corr, vol. abs/1807.04596, 2018.
    [Bibtex]
    @article{DBLP:journals/corr/abs-1807-04596,
    author = {Mat{\'{\i}}as Toro and
    Elizabeth Labrada and
    {\'{E}}ric Tanter},
    title = {Gradual Parametricity, Revisited},
    journal = {CoRR},
    volume = {abs/1807.04596},
    year = {2018},
    url = {http://arxiv.org/abs/1807.04596},
    archiveprefix = {arXiv},
    eprint = {1807.04596},
    timestamp = {Mon, 13 Aug 2018 16:46:42 +0200},
    biburl = {https://dblp.org/rec/bib/journals/corr/abs-1807-04596},
    bibsource = {dblp computer science bibliography, https://dblp.org}
    }
  • [DOI] W. J. Bowman, Y. Cong, N. Rioux, and A. Ahmed, “Type-preserving CPS translation of sigma and pi types is not not possible,” PACMPL, vol. 2, iss. {POPL}, p. 22:1–22:33, 2018.
    [Bibtex]
    @article{DBLP:journals/pacmpl/BowmanCRA18,
    author = {William J. Bowman and
    Youyou Cong and
    Nick Rioux and
    Amal Ahmed},
    title = {Type-preserving {CPS} translation of Sigma and Pi types
    is not not possible},
    journal = {{PACMPL}},
    volume = {2},
    number = {{POPL}},
    pages = {22:1--22:33},
    year = {2018},
    ee = {https://doi.org/10.1145/3158110},
    doi = {10.1145/3158110},
    timestamp = {Tue, 06 Nov 2018 12:51:05 +0100},
    biburl = {https://dblp.org/rec/bib/journals/pacmpl/BowmanCRA18},
    bibsource = {dblp computer science bibliography, https://dblp.org},
    url = {https://www.williamjbowman.com/resources/cps-sigma.pdf}
    }
  • [DOI] W. J. Bowman and A. Ahmed, “Typed closure conversion for the calculus of constructions,” in Proceedings of the 39th ACM SIGPLAN conference on programming language design and implementation, PLDI 2018, philadelphia, pa, usa, june 18-22, 2018, 2018, p. 797–811.
    [Bibtex]
    @inproceedings{DBLP:conf/pldi/BowmanA18,
    author = {William J. Bowman and
    Amal Ahmed},
    editor = {Jeffrey S. Foster and
    Dan Grossman},
    title = {Typed closure conversion for the calculus of constructions},
    booktitle = {Proceedings of the 39th {ACM} {SIGPLAN} Conference on Programming
    Language Design and Implementation, {PLDI} 2018, Philadelphia, PA,
    USA, June 18-22, 2018},
    pages = {797--811},
    publisher = {{ACM}},
    year = {2018},
    url = {https://doi.org/10.1145/3192366.3192372},
    doi = {10.1145/3192366.3192372},
    timestamp = {Wed, 21 Nov 2018 12:44:27 +0100},
    biburl = {https://dblp.org/rec/bib/conf/pldi/BowmanA18},
    bibsource = {dblp computer science bibliography, https://dblp.org}
    }
  • [DOI] O. Flückiger, G. Scherer, M. -, A. Goel, A. Ahmed, and J. Vitek, “Correctness of speculative optimizations with dynamic deoptimization,” PACMPL, vol. 2, iss. {POPL}, p. 49:1–49:28, 2018.
    [Bibtex]
    @article{DBLP:journals/pacmpl/FluckigerSYGAV18,
    author = {Olivier Fl{\"{u}}ckiger and
    Gabriel Scherer and
    Ming{-}Ho Yee and
    Aviral Goel and
    Amal Ahmed and
    Jan Vitek},
    title = {Correctness of speculative optimizations with dynamic deoptimization},
    journal = {{PACMPL}},
    volume = {2},
    number = {{POPL}},
    pages = {49:1--49:28},
    year = {2018},
    ee = {https://doi.org/10.1145/3158137},
    doi = {10.1145/3158137},
    timestamp = {Tue, 06 Nov 2018 12:51:05 +0100},
    biburl = {https://dblp.org/rec/bib/journals/pacmpl/FluckigerSYGAV18},
    bibsource = {dblp computer science bibliography, https://dblp.org},
    url = {https://arxiv.org/abs/1711.03050}
    }
  • [DOI] M. S. New and A. Ahmed, “Graduality from embedding-projection pairs,” PACMPL, vol. 2, iss. {ICFP}, p. 73:1–73:30, 2018.
    [Bibtex]
    @article{DBLP:journals/pacmpl/NewA18,
    author = {Max S. New and
    Amal Ahmed},
    title = {Graduality from embedding-projection pairs},
    journal = {{PACMPL}},
    volume = {2},
    number = {{ICFP}},
    pages = {73:1--73:30},
    year = {2018},
    url = {https://doi.org/10.1145/3236768},
    doi = {10.1145/3236768},
    timestamp = {Wed, 21 Nov 2018 12:44:28 +0100},
    biburl = {https://dblp.org/rec/bib/journals/pacmpl/NewA18},
    bibsource = {dblp computer science bibliography, https://dblp.org}
    }
  • [DOI] G. Scherer, M. S. New, N. Rioux, and A. Ahmed, “Fabulous interoperability for ML and a linear language,” in Foundations of software science and computation structures – 21st international conference, FOSSACS 2018, held as part of the european joint conferences on theory and practice of software, ETAPS 2018, thessaloniki, greece, april 14-20, 2018, proceedings, 2018, p. 146–162.
    [Bibtex]
    @inproceedings{DBLP:conf/fossacs/SchererNRA18,
    author = {Gabriel Scherer and
    Max S. New and
    Nick Rioux and
    Amal Ahmed},
    editor = {Christel Baier and
    Ugo Dal Lago},
    title = {FabULous Interoperability for {ML} and a Linear Language},
    booktitle = {Foundations of Software Science and Computation Structures - 21st
    International Conference, {FOSSACS} 2018, Held as Part of the European
    Joint Conferences on Theory and Practice of Software, {ETAPS} 2018,
    Thessaloniki, Greece, April 14-20, 2018, Proceedings},
    series = {Lecture Notes in Computer Science},
    volume = {10803},
    pages = {146--162},
    publisher = {Springer},
    year = {2018},
    url = {https://doi.org/10.1007/978-3-319-89366-2\_8},
    doi = {10.1007/978-3-319-89366-2\_8},
    timestamp = {Tue, 26 Jun 2018 14:10:46 +0200},
    biburl = {https://dblp.org/rec/bib/conf/fossacs/SchererNRA18},
    bibsource = {dblp computer science bibliography, https://dblp.org}
    }
  • A. Weiss, D. Patterson, and A. Ahmed, “Rust distilled: an expressive tower of languages,” Corr, vol. abs/1806.02693, 2018.
    [Bibtex]
    @article{DBLP:journals/corr/abs-1806-02693,
    author = {Aaron Weiss and
    Daniel Patterson and
    Amal Ahmed},
    title = {Rust Distilled: An Expressive Tower of Languages},
    journal = {CoRR},
    volume = {abs/1806.02693},
    year = {2018},
    url = {http://arxiv.org/abs/1806.02693},
    archiveprefix = {arXiv},
    eprint = {1806.02693},
    timestamp = {Mon, 13 Aug 2018 16:47:54 +0200},
    biburl = {https://dblp.org/rec/bib/journals/corr/abs-1806-02693},
    bibsource = {dblp computer science bibliography, https://dblp.org}
    }
  • [DOI] A. Ahmed, D. Garg, C. Hritcu, and F. Piessens, “Secure Compilation (Dagstuhl Seminar 18201),” Dagstuhl reports, vol. 8, iss. 5, p. 1–30, 2018.
    [Bibtex]
    @article{dagstuhl2018,
    author = {Amal Ahmed and Deepak Garg and Catalin Hritcu and Frank Piessens},
    title = {{Secure Compilation (Dagstuhl Seminar 18201)}},
    pages = {1--30},
    journal = {Dagstuhl Reports},
    issn = {2192-5283},
    year = {2018},
    volume = {8},
    number = {5},
    editor = {Amal Ahmed and Deepak Garg and Catalin Hritcu and Frank Piessens},
    publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
    address = {Dagstuhl, Germany},
    url = {http://drops.dagstuhl.de/opus/volltexte/2018/9891},
    urn = {urn:nbn:de:0030-drops-98911},
    doi = {10.4230/DagRep.8.5.1},
    annote = {Keywords: secure compilation, low-level attacks, source-level reasoning, attacker models, full abstraction, hyperproperties, enforcement mechanisms, }
    }
  • C. Abate, A. Azevedo de Amorim, R. Blanco, A. N. Evans, G. Fachini, C. Hritcu, T. Laurent, B. C. Pierce, M. Stronati, and A. Tolmach, “When good components go bad: formally secure compilation despite dynamic compromise,” in 25th acm conference on computer and communications security (ccs), 2018, p. 1351–1368.
    [Bibtex]
    @inproceedings{AbateABEFHLPST18,
    author = {Carmine Abate and
    Arthur {Azevedo de Amorim} and
    Roberto Blanco and
    Ana Nora Evans and
    Guglielmo Fachini and
    Catalin Hritcu and
    Th\'eo Laurent and
    Benjamin C. Pierce and
    Marco Stronati and
    Andrew Tolmach},
    title = {When Good Components Go Bad:
    Formally Secure Compilation Despite Dynamic Compromise},
    booktitle = {25th ACM Conference on
    Computer and Communications Security (CCS)},
    shortbooktitle = {CCS},
    url = {https://arxiv.org/abs/1802.00588},
    year = {2018},
    month = oct,
    pages = {1351--1368},
    publisher = {{ACM}}
    }
  • [DOI] A. Azevedo de Amorim, C. Hritcu, and B. C. Pierce, “The meaning of memory safety,” in 7th international conference on principles of security and trust (POST), 2018, p. 79–105.
    [Bibtex]
    @inproceedings{memory-safety,
    author = {Arthur {Azevedo de Amorim} and
    Catalin Hritcu and
    Benjamin C. Pierce},
    title = {The Meaning of Memory Safety},
    booktitle = {7th International Conference on
    Principles of Security and Trust ({POST})},
    pages = {79--105},
    doi = {10.1007/978-3-319-89722-6\_4},
    url = {https://arxiv.org/abs/1705.07354},
    year = {2018},
    month = apr
    }
  • D. Ahman, “Handling fibred algebraic effects,” PACMPL, vol. 2, iss. {POPL}, 2018.
    [Bibtex]
    @article{Ahman18,
    author = {Danel Ahman},
    title = {Handling Fibred Algebraic Effects},
    journal = {{PACMPL}},
    volume = {2},
    number = {{POPL}},
    year = {2018},
    month = jan,
    url = {https://danelahman.github.io/papers/popl18.pdf}
    }
  • [DOI] N. Grimm, K. Maillard, C. Fournet, C. Hritcu, M. Maffei, J. Protzenko, T. Ramananandro, A. Rastogi, N. Swamy, and S. Zanella-Béguelin, “A monadic framework for relational verification: applied to information security, program equivalence, and optimizations,” in 7th acm sigplan international conference on certified programs and proofs (cpp), 2018, p. 130–145.
    [Bibtex]
    @inproceedings{relational,
    author = {Niklas Grimm and
    Kenji Maillard and
    C\'edric Fournet and
    Catalin Hritcu and
    Matteo Maffei and
    Jonathan Protzenko and
    Tahina Ramananandro and
    Aseem Rastogi and
    Nikhil Swamy and
    Santiago {Zanella-B\'eguelin}},
    title = {A Monadic Framework for Relational Verification: Applied to
    Information Security, Program Equivalence, and Optimizations},
    booktitle = {7th ACM SIGPLAN International Conference on
    Certified Programs and Proofs (CPP)},
    shortbooktitle = {CPP},
    url = {https://arxiv.org/abs/1703.00055},
    month = jan,
    year = {2018},
    isbn = {978-1-4503-5586-5},
    location = {Los Angeles, CA, USA},
    pages = {130--145},
    numpages = {16},
    ee = {http://doi.acm.org/10.1145/3167090},
    doi = {10.1145/3167090},
    acmid = {3167090},
    publisher = {ACM}
    }
  • D. Ahman, C. Fournet, C. Hritcu, K. Maillard, A. Rastogi, and N. Swamy, “Recalling a witness: foundations and applications of monotonic state,” PACMPL, vol. 2, iss. {POPL}, p. 65:1–65:30, 2018.
    [Bibtex]
    @article{preorders,
    author = {Danel Ahman and
    C\'edric Fournet and
    Catalin Hritcu and
    Kenji Maillard and
    Aseem Rastogi and
    Nikhil Swamy},
    title = {Recalling a Witness: Foundations and Applications of Monotonic State},
    journal = {{PACMPL}},
    volume = {2},
    number = {{POPL}},
    pages = {65:1--65:30},
    year = {2018},
    month = jan,
    url = {https://arxiv.org/abs/1707.02466}
    }
  • K. Bhargavan, I. Boureanu, A. D. -, P. -, and C. Onete, “A formal treatment of accountable proxying over TLS,” in IEEE symposium on security and privacy (oakland), 2018, p. 799–816.
    [Bibtex]
    @inproceedings{DBLP:conf/sp/BhargavanBDFO18,
    author = {Karthikeyan Bhargavan and Ioana Boureanu and Antoine Delignat{-}Lavaud and Pierre{-}Alain Fouque and Cristina Onete},
    title = {A Formal Treatment of Accountable Proxying Over {TLS}},
    booktitle = {{IEEE} Symposium on Security and Privacy (Oakland)},
    pages = {799--816},
    year = {2018}
    }
  • [PDF] K. Bhargavan, R. Barnes, and E. Rescorla, TreeKEM: Asynchronous Decentralized Key Management for Large Dynamic Groups, 2018.
    [Bibtex]
    @misc{BBR18,
    author = {Karthikeyan Bhargavan and Richard Barnes and Eric Rescorla},
    title = {{TreeKEM: Asynchronous Decentralized Key Management
    for Large Dynamic Groups}},
    year = 2018,
    month = May,
    note = {Published at \url{https://mailarchive.ietf.org/arch/msg/mls/e3ZKNzPC7Gxrm3Wf0q96dsLZoD8}},
    pdf = {http://prosecco.inria.fr/personal/karthik/pubs/treekem.pdf},
    url = {http://prosecco.inria.fr/personal/karthik/pubs/treekem.pdf}
    }

2017

  • [PDF] [DOI] N. Kobeissi, K. Bhargavan, and B. Blanchet, “Automated Verification for Secure Messaging Protocols and Their Implementations: A Symbolic and Computational Approach,” in 2nd IEEE European Symposium on Security and Privacy, Paris, France, 2017, pp. 435-450.
    [Bibtex]
    @inproceedings{kobeissi:hal-01575923,
    title = {{Automated Verification for Secure Messaging Protocols and Their Implementations: A Symbolic and Computational Approach}},
    author = {Kobeissi, Nadim and Bhargavan, Karthikeyan and Blanchet, Bruno},
    url = {https://hal.inria.fr/hal-01575923},
    booktitle = {{2nd IEEE European Symposium on Security and Privacy}},
    address = {Paris, France},
    pages = {435 - 450},
    year = {2017},
    month = Apr,
    doi = {10.1109/EuroSP.2017.38},
    pdf = {https://hal.inria.fr/hal-01575923/file/KobeissiBhargavanBlanchetEuroSP17.pdf},
    hal_id = {hal-01575923},
    hal_version = {v1}
    }
  • D. Ahman and T. Uustalu, “Taking updates seriously,” in Proceedings of the 6th international workshop on bidirectional transformations co-located with the european joint conferences on theory and practice of software, bx@etaps 2017, uppsala, sweden, april 29, 2017., 2017, p. 59–73.
    [Bibtex]
    @inproceedings{DBLP:conf/etaps/AhmanU17,
    author = {Danel Ahman and
    Tarmo Uustalu},
    title = {Taking Updates Seriously},
    booktitle = {Proceedings of the 6th International Workshop on Bidirectional Transformations
    co-located with The European Joint Conferences on Theory and Practice
    of Software, BX@ETAPS 2017, Uppsala, Sweden, April 29, 2017.},
    pages = {59--73},
    year = {2017},
    url = {http://ceur-ws.org/Vol-1827/paper11.pdf},
    biburl = {http://dblp.org/rec/bib/conf/etaps/AhmanU17},
    bibsource = {dblp computer science bibliography, http://dblp.org}
    }
  • [DOI] J. Protzenko, J. Zinzindohoué, A. Rastogi, T. Ramananandro, P. Wang, S. Zanella-Béguelin, A. Delignat-Lavaud, C. Hritcu, K. Bhargavan, C. Fournet, and N. Swamy, “Verified low-level programming embedded in F*,” PACMPL, vol. 1, iss. {ICFP}, p. 17:1–17:29, 2017.
    [Bibtex]
    @article{lowstar,
    author = {Jonathan Protzenko and
    Jean-Karim Zinzindohou\'e and
    Aseem Rastogi and
    Tahina Ramananandro and
    Peng Wang and
    Santiago {Zanella-B\'eguelin} and
    Antoine Delignat-Lavaud and
    Catalin Hritcu and
    Karthikeyan Bhargavan and
    C\'edric Fournet and
    Nikhil Swamy},
    title = {Verified Low-Level Programming Embedded in {F*}},
    journal = {{PACMPL}},
    volume = {1},
    number = {{ICFP}},
    pages = {17:1--17:29},
    year = {2017},
    month = sep,
    ee = {http://doi.acm.org/10.1145/3110261},
    doi = {10.1145/3110261},
    url = {http://arxiv.org/abs/1703.00053}
    }
  • K. Bhargavan, B. Bond, A. Delignat-Lavaud, C. Fournet, C. Hawblitzel, C. Hritcu, S. Ishtiaq, M. Kohlweiss, R. Leino, J. Lorch, K. Maillard, J. Pang, B. Parno, J. Protzenko, T. Ramananandro, A. Rane, A. Rastogi, N. Swamy, L. Thompson, P. Wang, S. Zanella-Béguelin, and J. Zinzindohoué, “Everest: towards a verified, drop-in replacement of HTTPS,” in 2nd summit on advances in programming languages (snapl), 2017.
    [Bibtex]
    @inproceedings{everest,
    author = {Karthikeyan Bhargavan and
    Barry Bond and
    Antoine Delignat-Lavaud and
    C\'edric Fournet and
    Chris Hawblitzel and
    Catalin Hritcu and
    Samin Ishtiaq and
    Markulf Kohlweiss and
    Rustan Leino and
    Jay Lorch and
    Kenji Maillard and
    Jianyang Pang and
    Bryan Parno and
    Jonathan Protzenko and
    Tahina Ramananandro and
    Ashay Rane and
    Aseem Rastogi and
    Nikhil Swamy and
    Laure Thompson and
    Perry Wang and
    Santiago Zanella-B\'eguelin and
    Jean-Karim Zinzindohou\'e},
    title = {Everest: Towards a Verified, Drop-in Replacement of {HTTPS}},
    booktitle = {2nd Summit on Advances in Programming Languages (SNAPL)},
    shortbooktitle = {SNAPL},
    month = may,
    year = 2017,
    url = {http://drops.dagstuhl.de/opus/volltexte/2017/7119/pdf/LIPIcs-SNAPL-2017-1.pdf}
    }
  • M. ‘i, B. Blanchet, and C. Fournet, “The applied pi calculus: mobile values, new names, and secure communication,” Journal of the acm, vol. 65, iss. 1, p. 1:1–1:41, 2017.
    [Bibtex]
    @article{AbadiBlanchetFournetJACM17,
    author = {Mart{\'\i}n Abadi and Bruno Blanchet and C{\'e}dric Fournet},
    title = {The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication},
    journal = {Journal of the ACM},
    year = {2017},
    volume = {65},
    number = {1},
    month = oct,
    pages = {1:1--1:41},
    articleno = {1},
    numpages = {41},
    url = {https://bblanche.gitlabpages.inria.fr/publications/AbadiBlanchetFournetJACM17.html}
    }
  • B. Blanchet, “Symbolic and computational mechanized verification of the ARINC823 avionic protocols,” in 30th ieee computer security foundations symposium (csf’17), 2017, p. 68–82.
    [Bibtex]
    @inproceedings{BlanchetCSF17,
    author = {Bruno Blanchet},
    title = {Symbolic and Computational Mechanized Verification of the {ARINC823} Avionic Protocols},
    booktitle = {30th IEEE Computer Security Foundations Symposium (CSF'17)},
    pages = {68--82},
    year = {2017},
    url = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetCSF17.html}
    }
  • B. Blanchet, “Symbolic and computational mechanized verification of the ARINC823 avionic protocols,” Inria, RR-9072, 2017.
    [Bibtex]
    @techreport{BlanchetInria17,
    author = {Bruno Blanchet},
    title = {Symbolic and Computational Mechanized Verification of the {ARINC823} Avionic Protocols},
    institution = {Inria},
    year = 2017,
    number = {RR-9072},
    url = {https://hal.inria.fr/hal-01527671}
    }
  • [DOI] D. Ahman, C. Hritcu, K. Maillard, G. Martínez, G. Plotkin, J. Protzenko, A. Rastogi, and N. Swamy, “Dijkstra monads for free,” in 44th acm sigplan symposium on principles of programming languages (popl), 2017, pp. 515-529.
    [Bibtex]
    @inproceedings{dm4free,
    author = {Danel Ahman and
    Catalin Hritcu and
    Kenji Maillard and
    Guido Mart\'inez and
    Gordon Plotkin and
    Jonathan Protzenko and
    Aseem Rastogi and
    Nikhil Swamy},
    title = {Dijkstra Monads for Free},
    booktitle = {44th ACM SIGPLAN Symposium on Principles of Programming
    Languages (POPL)},
    shortbooktitle = {POPL},
    year = {2017},
    month = jan,
    ee = {https://dl.acm.org/citation.cfm?id=3009878},
    doi = {10.1145/3009837.3009878},
    url = {https://www.fstar-lang.org/papers/dm4free/},
    pages = {515-529},
    publisher = {ACM},
    acceptance = {64/279=0.23}
    }
  • [DOI] L. Lampropoulos, D. Gallois-Wong, C. Hritcu, J. Hughes, B. C. Pierce, and Li-yao, “Beginner’s Luck: a language for random generators,” in 44th acm sigplan symposium on principles of programming languages (popl), 2017, pp. 114-129.
    [Bibtex]
    @inproceedings{beginners-luck,
    author = {Leonidas Lampropoulos and
    Diane Gallois-Wong and
    Catalin Hritcu and
    John Hughes and
    Benjamin C. Pierce and
    {Li-yao} Xia},
    title = {Beginner's {Luck}: A Language for Random Generators},
    booktitle = {44th ACM SIGPLAN Symposium on Principles of Programming
    Languages (POPL)},
    shortbooktitle = {POPL},
    year = {2017},
    month = jan,
    url = {https://arxiv.org/abs/1607.05443},
    ee = {https://dl.acm.org/citation.cfm?id=3009868},
    doi = {10.1145/3009837.3009868},
    pages = {114-129},
    publisher = {ACM},
    acceptance = {64/279=0.23}
    }
  • B. Beurdouche, K. Bhargavan, A. Delignat-Lavaud, C. Fournet, M. Kohlweiss, A. Pironti, P. Strub, and J. K. Zinzindohoue, “A messy state of the union: taming the composite state machines of tls,” Communications of the acm, vol. 60, iss. 2, p. 99–107, 2017.
    [Bibtex]
    @article{Beurdouche:2017:MSU:3042068.3023357,
    author = {Beurdouche, Benjamin and Bhargavan, Karthikeyan and Delignat-Lavaud, Antoine and Fournet, C{\'e}dric and Kohlweiss, Markulf and Pironti, Alfredo and Strub, Pierre-Yves and Zinzindohoue, Jean Karim},
    title = {A Messy State of the Union: Taming the Composite State Machines of TLS},
    journal = {Communications of the ACM},
    volume = {60},
    number = {2},
    year = {2017},
    pages = {99--107}
    }
  • N. Kobeissi, K. Bhargavan, and B. Blanchet, “Automated verification for secure messaging protocols and their implementations: a symbolic and computational approach,” in IEEE european symposium on security and privacy (euros&p), 2017, p. 435–450.
    [Bibtex]
    @inproceedings{proscript,
    author = {Nadim Kobeissi and Karthikeyan Bhargavan and Bruno Blanchet},
    title = {Automated Verification for Secure Messaging Protocols and their Implementations: A Symbolic and Computational Approach},
    booktitle = {{IEEE} European Symposium on Security and Privacy (EuroS{\&}P)},
    year = {2017},
    pages = {435--450}
    }
  • K. Bhargavan, I. Carlson, P. Fouque, C. Onete, and B. Richard, “Content delivery over tls: a cryptographic analysis of keyless ssl,” in IEEE european symposium on security and privacy (euros&p), 2017.
    [Bibtex]
    @inproceedings{keyless,
    author = {K. Bhargavan and I. Carlson and P. Fouque and C. Onete and B. Richard},
    title = {Content delivery over TLS: a cryptographic analysis of Keyless SSL},
    booktitle = {{IEEE} European Symposium on Security and Privacy (EuroS{\&}P)},
    year = {2017}
    }
  • K. Bhargavan, A. Delignat-Lavaud, and N. Kobeissi, “Formal modeling and verification for domain validation and acme,” in Financial cryptography and data security (fc), 2017.
    [Bibtex]
    @inproceedings{acme,
    author = {Karthikeyan Bhargavan and Antoine Delignat-Lavaud and Nadim Kobeissi},
    title = {Formal Modeling and Verification for Domain Validation and ACME},
    booktitle = {Financial Cryptography and Data Security (FC)},
    year = {2017}
    }
  • K. Bhargavan, A. Delignat-Lavaud, C. Fournet, M. Kohlweiss, J. Pan, J. Protzenko, A. Rastogi, N. Swamy, S. Zanella-Béguelin, and J. K. Zinzindohoué, “Implementing and proving the TLS 1.3 record layer,” in IEEE symposium on security and privacy (oakland), 2017.
    [Bibtex]
    @inproceedings{mitls-record,
    author = {Karthikeyan Bhargavan and Antoine Delignat-Lavaud and C\'edric Fournet and Markulf Kohlweiss and Jianyang Pan and Jonathan Protzenko and Aseem Rastogi and Nikhil Swamy and Santiago Zanella-B\'eguelin and Jean Karim Zinzindohou\'e},
    title = {Implementing and Proving the {TLS} 1.3 Record Layer},
    booktitle = {{IEEE} Symposium on Security and Privacy (Oakland)},
    year = {2017}
    }
  • K. Bhargavan, B. Blanchet, and N. Kobeissi, “Verified models and reference implementations for the TLS 1.3 standard candidate,” in IEEE symposium on security and privacy (oakland), 2017, p. 483–503.
    [Bibtex]
    @inproceedings{reftls,
    author = {Karthikeyan Bhargavan and Bruno Blanchet and Nadim Kobeissi},
    title = {Verified Models and Reference Implementations for the {TLS} 1.3 Standard Candidate },
    booktitle = {{IEEE} Symposium on Security and Privacy (Oakland)},
    year = {2017},
    pages = {483--503}
    }
  • K. Bhargavan, B. Blanchet, and N. Kobeissi, “Verified models and reference implementations for the TLS 1.3 standard candidate,” Inria, RR-9040, 2017.
    [Bibtex]
    @techreport{reftlsInria2017,
    author = {Karthikeyan Bhargavan and Bruno Blanchet and Nadim Kobeissi},
    title = {Verified Models and Reference Implementations for the {TLS} 1.3 Standard Candidate},
    institution = {Inria},
    year = 2017,
    number = {RR-9040},
    url = {https://hal.inria.fr/hal-01528752}
    }
  • J. K. Zinzindohoué, K. Bhargavan, J. Protzenko, and B. Beurdouche, “Hacl*: A verified modern cryptographic library,” in Proceedings of the 2017 ACM SIGSAC conference on computer and communications security, CCS 2017, dallas, tx, usa, october 30 – november 03, 2017, 2017, p. 1789–1806.
    [Bibtex]
    @inproceedings{DBLP:conf/ccs/ZinzindohoueBPB17,
    author = {Jean Karim Zinzindohou{\'{e}} and
    Karthikeyan Bhargavan and
    Jonathan Protzenko and
    Benjamin Beurdouche},
    title = {HACL*: {A} Verified Modern Cryptographic Library},
    booktitle = {Proceedings of the 2017 {ACM} {SIGSAC} Conference on Computer and
    Communications Security, {CCS} 2017, Dallas, TX, USA, October 30 -
    November 03, 2017},
    pages = {1789--1806},
    year = {2017},
    url = {http://doi.acm.org/10.1145/3133956.3134043}
    }
  • [PDF] [DOI] C. Troncoso, M. Isaakidis, G. Danezis, and H. Halpin, “Systematizing Decentralization and Privacy: Lessons from 15 Years of Research and Deployments,” Proceedings on Privacy Enhancing Technologies, vol. 2017, iss. 4, pp. 307-329, 2017.
    [Bibtex]
    @article{troncoso:hal-01673295,
    title = {{Systematizing Decentralization and Privacy: Lessons from 15 Years of Research and Deployments}},
    author = {Troncoso, Carmela and Isaakidis, Marios and Danezis, George and Halpin, Harry},
    url = {https://hal.inria.fr/hal-01673295},
    journal = {{Proceedings on Privacy Enhancing Technologies}},
    publisher = {{De Gruyter Open}},
    volume = {2017},
    number = {4},
    pages = {307 - 329},
    year = {2017},
    month = Oct,
    doi = {10.1515/popets-2017-0052},
    keywords = {Decentralization ; Privacy ; Peer-to-peer ; Systematization of Knowledge},
    pdf = {https://hal.inria.fr/hal-01673295/file/paper87-2017-4-source.pdf},
    hal_id = {hal-01673295},
    hal_version = {v1}
    }
  • [PDF] H. Halpin, “The Crisis of Standardizing DRM: The Case of W3C Encrypted Media Extensions,” in Security, Privacy, and Applied Cryptography Engineering (SPACE 2017), Goa, India, 2017.
    [Bibtex]
    @inproceedings{halpin:hal-01673296,
    title = {{The Crisis of Standardizing DRM: The Case of W3C Encrypted Media Extensions}},
    author = {Halpin, Harry},
    url = {https://hal.inria.fr/hal-01673296},
    booktitle = {{Security, Privacy, and Applied Cryptography Engineering (SPACE 2017)}},
    address = {Goa, India},
    year = {2017},
    month = Dec,
    keywords = {Digital Rights Management ; W3C ; security ; privacy ; standardization},
    pdf = {https://hal.inria.fr/hal-01673296/file/drm.pdf},
    hal_id = {hal-01673296},
    hal_version = {v1}
    }
  • [PDF] H. Halpin, “A Roadmap for High Assurance Cryptography,” in Foundations and Practice of Security, Nancy, France, 2017.
    [Bibtex]
    @inproceedings{halpin:hal-01673294,
    title = {{A Roadmap for High Assurance Cryptography}},
    author = {Halpin, Harry},
    url = {https://hal.inria.fr/hal-01673294},
    booktitle = {{Foundations and Practice of Security}},
    address = {Nancy, France},
    year = {2017},
    month = Oct,
    keywords = {high assurance cryptography ; formal verification ; primitives ; security API},
    pdf = {https://hal.inria.fr/hal-01673294/file/paper.pdf},
    hal_id = {hal-01673294},
    hal_version = {v1}
    }
  • [PDF] H. Halpin and M. Piekarska, Introduction to Security and Privacy on the Blockchain, 2017.
    [Bibtex]
    @misc{halpin:hal-01673293,
    title = {{Introduction to Security and Privacy on the Blockchain}},
    author = {Halpin, Harry and Piekarska, Marta},
    url = {https://hal.inria.fr/hal-01673293},
    howpublished = {{2017 IEEE European Symposium on Security and Privacy Workshops (EuroS\&P Workshops 2017)}},
    year = {2017},
    month = Apr,
    pdf = {https://hal.inria.fr/hal-01673293/file/intro_final.pdf},
    hal_id = {hal-01673293},
    hal_version = {v1}
    }
  • [PDF] [DOI] H. Halpin, “NEXTLEAP: Decentralizing Identity with Privacy for Secure Messaging,” in Proceedings of Availability, Reliability, and Security (ARES), Reggio Calabria, Italy, 2017.
    [Bibtex]
    @inproceedings{halpin:hal-01673292,
    title = {{NEXTLEAP: Decentralizing Identity with Privacy for Secure Messaging}},
    author = {Halpin, Harry},
    url = {https://hal.inria.fr/hal-01673292},
    booktitle = {{Proceedings of Availability, Reliability, and Security (ARES)}},
    address = {Reggio Calabria, Italy},
    year = {2017},
    month = Aug,
    doi = {10.1145/3098954.3104056},
    keywords = {decentralization ; privacy ; secure messaging ; identity ; anonymity},
    pdf = {https://hal.inria.fr/hal-01673292/file/ares2017.pdf},
    hal_id = {hal-01673292},
    hal_version = {v1}
    }
  • [PDF] H. Halpin, “Semantic Insecurity: Security and the Semantic Web,” in Society, Privacy and the Semantic Web – Policy and Technology (PrivOn 2017), Vienna, Austria, 2017.
    [Bibtex]
    @inproceedings{halpin:hal-01673291,
    title = {{Semantic Insecurity: Security and the Semantic Web}},
    author = {Halpin, Harry},
    url = {https://hal.inria.fr/hal-01673291},
    booktitle = {{ Society, Privacy and the Semantic Web - Policy and Technology (PrivOn 2017)}},
    address = {Vienna, Austria},
    year = {2017},
    month = Oct,
    keywords = {security ; TLS ; WebID ; Semantic Web ; RDF},
    pdf = {https://hal.inria.fr/hal-01673291/file/main.pdf},
    hal_id = {hal-01673291},
    hal_version = {v1}
    }

2016

  • B. Blanchet, “Modeling and verifying security protocols with the applied pi calculus and ProVerif,” Foundations and trends in privacy and security, vol. 1, iss. 1–2, p. 1–135, 2016.
    [Bibtex]
    @article{BlanchetFnTPS16,
    author = {Bruno Blanchet},
    title = {Modeling and Verifying Security Protocols with the Applied Pi Calculus and {P}ro{V}erif},
    journal = {Foundations and Trends in Privacy and Security},
    year = {2016},
    volume = {1},
    number = {1--2},
    pages = {1--135},
    month = oct,
    abstract = {ProVerif is an automatic symbolic protocol verifier. It supports a
    wide range of cryptographic primitives, defined by rewrite rules or
    by equations. It can prove various security properties: secrecy,
    authentication, and process equivalences,
    for an unbounded message space and an unbounded number of sessions.
    It takes as input a description of the protocol to verify in a
    dialect of the applied pi calculus, an extension of the pi calculus
    with cryptography. It automatically translates this protocol description
    into Horn clauses and determines whether
    the desired security properties hold by resolution on these clauses.
    This survey presents an overview of the research on
    ProVerif.},
    url = {http://dx.doi.org/10.1561/3300000004}
    }
  • G. Bana and M. Okada, “Semantics for “enough-certainty” and fitting’s embedding of classical logic in s4,” in 25th eacsl annual conference on computer science logic (csl 2016), 2016, p. 34:1–34:18.
    [Bibtex]
    @inproceedings{ban:oka:csl:16,
    author = {Gergei Bana and Mitsuhiro Okada},
    title = {Semantics for ``Enough-Certainty'' and Fitting's Embedding of Classical Logic in S4},
    booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
    year = {2016},
    pages = {34:1--34:18},
    volume = 62,
    publisher = {Dagstuhl}
    }
  • M. ‘i, B. Blanchet, and C. Fournet, The applied pi calculus: mobile values, new names, and secure communication, 2016.
    [Bibtex]
    @misc{appliedpi,
    author = {Mart{\'\i}n Abadi and Bruno Blanchet and C{\'e}dric Fournet},
    title = {The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication},
    howpublished = {Report arXiv:1609.03003v1},
    month = sep,
    year = 2016,
    abstract = {We study the interaction of the programming construct ``new'', which generates statically scoped names, with communication via messages on channels. This interaction is crucial in security protocols, which are the main motivating examples for our work, it also appears in other programming-language contexts.
    We define the applied pi calculus, a simple, general extension of the pi calculus in which values can be formed from names via the application of built-in functions, subject to equations, and be sent as messages. (In contrast, the pure pi calculus lacks built-in functions, its only messages are atomic names.) We develop semantics and proof techniques for this extended language and apply them in reasoning about security protocols.
    This paper essentially subsumes the conference paper that introduced the applied pi calculus in 2001. It fills gaps, incorporates improvements, and further explains and studies the applied pi calculus. Since 2001, the applied pi calculus has been the basis for much further work, described in many research publications and sometimes embodied in useful software, such as the tool ProVerif, which relies on the applied pi calculus to support the specification and automatic analysis of security protocols. Although this paper does not aim to be a complete review of the subject, it benefits from that further work and provides better foundations for some of it. In particular, the applied pi calculus has evolved through its implementation in ProVerif, and the present definition reflects that evolution.},
    url = {http://arxiv.org/abs/1609.03003v1}
    }
  • B. Blanchet and B. Smyth, “Automated reasoning for equivalences in the applied pi calculus with barriers,” in 29th ieee computer security foundations symposium (csf’16), Lisboa, Portugal, 2016, p. 310–324.
    [Bibtex]
    @inproceedings{BlanchetSmythCSF16,
    author = {Bruno Blanchet and Ben Smyth},
    title = {Automated reasoning for equivalences in the applied pi calculus with barriers},
    booktitle = {29th IEEE Computer Security Foundations Symposium (CSF'16)},
    year = 2016,
    pages = {310--324},
    month = jun,
    address = {Lisboa, Portugal},
    publisher = {IEEE},
    url = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetSmythCSF16.html},
    note = {Long version available at \url{https://hal.inria.fr/hal-01306440}}
    }
  • B. Blanchet and B. Smyth, “Automated reasoning for equivalences in the applied pi calculus with barriers,” Inria, Research report RR-8906, 2016.
    [Bibtex]
    @techreport{BlanchetSmythInria16,
    author = {Bruno Blanchet and Ben Smyth},
    title = {Automated reasoning for equivalences in the applied pi calculus with barriers},
    institution = {Inria},
    year = 2016,
    type = {Research report},
    number = {RR-8906},
    month = apr,
    url = {https://hal.inria.fr/hal-01306440},
    note = {Available at \url{https://hal.inria.fr/hal-01306440}}
    }
  • G. Bana, “On the formal consistency of the principal principle,” Philosophy of science, vol. 83, iss. 5, p. 988–1001, 2016.
    [Bibtex]
    @article{bana:phil:16,
    author = {Gergei Bana},
    title = {On the Formal Consistency of the Principal Principle},
    journal = {Philosophy of Science},
    publisher = {University of Chicago Press},
    volume = {83},
    number = {5},
    year = {2016},
    pages = {988--1001}
    }
  • [DOI] Y. Juglaret, C. Hritcu, A. Azevedo de Amorim, B. Eng, and B. C. Pierce, “Beyond good and evil: formalizing the security guarantees of compartmentalizing compilation,” in 29th ieee symposium on computer security foundations (csf), 2016, p. 45–60.
    [Bibtex]
    @inproceedings{beyond-good-and-evil,
    author = {Yannis Juglaret and
    Catalin Hritcu and
    Arthur {Azevedo de Amorim} and
    Boris Eng and
    Benjamin C. Pierce},
    title = {Beyond Good and Evil: Formalizing the Security Guarantees
    of Compartmentalizing Compilation},
    booktitle = {29th IEEE Symposium on Computer Security Foundations (CSF)},
    shortbooktitle = {CSF},
    year = {2016},
    month = jul,
    publisher = {IEEE Computer Society Press},
    url = {http://arxiv.org/abs/1602.04503},
    acceptance = {31/87=0.36},
    key = {Conference Papers},
    pages = {45--60},
    doi = {10.1109/CSF.2016.11}
    }
  • A. Azevedo de Amorim, N. Collins, A. DeHon, D. Demange, C. Hritcu, D. Pichardie, B. C. Pierce, R. Pollack, and A. Tolmach, “A verified information-flow architecture,” Journal of computer security (jcs); special issue on verified information flow security, vol. 24, iss. 6, p. 689–734, 2016.
    [Bibtex]
    @article{ver_ifc_jcs,
    title = {A Verified Information-Flow Architecture},
    author = {
    Arthur {Azevedo de Amorim} and
    Nathan Collins and
    Andr\'e DeHon and
    Delphine Demange and
    Catalin Hritcu and
    David Pichardie and
    Benjamin C. Pierce and
    Randy Pollack and
    Andrew Tolmach
    },
    journal = {Journal of Computer Security (JCS);
    Special Issue on Verified Information Flow Security},
    volume = {24},
    number = {6},
    pages = {689--734},
    year = {2016},
    month = dec,
    ee = {http://content.iospress.com/articles/journal-of-computer-security/jcs15784},
    url = {http://arxiv.org/abs/1509.06503}
    }
  • N. Swamy, C. Hritcu, C. Keller, A. Rastogi, A. Delignat-Lavaud, S. Forest, K. Bhargavan, C. Fournet, P. Strub, M. Kohlweiss, J. Zinzindohoue, and S. Zanella-Béguelin, “Dependent types and multi-monadic effects in F*,” in 43rd acm sigplan-sigact symposium on principles of programming languages (popl), 2016, pp. 256-270.
    [Bibtex]
    @inproceedings{fstar-popl2016,
    author = {Nikhil Swamy and
    Catalin Hritcu and
    Chantal Keller and
    Aseem Rastogi and
    Antoine Delignat-Lavaud and
    Simon Forest and
    Karthikeyan Bhargavan and
    C\'{e}dric Fournet and
    Pierre-Yves Strub and
    Markulf Kohlweiss and
    Jean-Karim Zinzindohoue and
    Santiago Zanella-B\'eguelin},
    title = {Dependent Types and Multi-Monadic Effects in {F*}},
    booktitle = {43rd ACM SIGPLAN-SIGACT
    Symposium on Principles of Programming Languages (POPL)},
    shortbooktitle = {POPL},
    pages = {256-270},
    publisher = {ACM},
    isbn = {978-1-4503-3549-2},
    month = jan,
    year = {2016},
    ee = {http://dx.doi.org/10.1145/2837614.2837655},
    url = {https://www.fstar-lang.org/papers/mumon/},
    acceptance = {59/253=0.23}
    }
  • [DOI] C. Hritcu, L. Lampropoulos, A. Spector-Zabusky, A. Azevedo de Amorim, M. Dénès, J. Hughes, B. C. Pierce, and D. Vytiniotis, “Testing noninterference, quickly,” Journal of functional programming (jfp); special issue for icfp 2013, vol. 26, p. e4 (62 pages), 2016.
    [Bibtex]
    @article{testing_ni_jfp,
    author = {Catalin Hritcu and
    Leonidas Lampropoulos and
    Antal Spector-Zabusky and
    Arthur {Azevedo de Amorim} and
    Maxime D\'{e}n\`{e}s and
    John Hughes and
    Benjamin C. Pierce and
    Dimitrios Vytiniotis},
    title = {Testing Noninterference, Quickly},
    journal = {Journal of Functional Programming (JFP); Special issue for ICFP 2013},
    shortjournal = {JFP},
    volume = {26},
    year = {2016},
    month = apr,
    issn = {1469-7653},
    pages = {e4 (62 pages)},
    doi = {http://dx.doi.org/10.1017/S0956796816000058},
    ee = {http://journals.cambridge.org/article_S0956796816000058},
    url = {http://arxiv.org/abs/1409.0393}
    }
  • K. Bhargavan and G. Leurent, “Transcript collision attacks: breaking authentication in tls, ike, and ssh,” in Proceedings of the ISOC network and distributed system security symposium (NDSS ’16), 2016.
    [Bibtex]
    @inproceedings{BhargavanL16,
    author = {Karthikeyan Bhargavan and Gaetan Leurent},
    title = {Transcript Collision Attacks: Breaking Authentication in TLS, IKE, and SSH},
    booktitle = {Proceedings of the {ISOC} Network and Distributed System Security Symposium ({NDSS} '16)},
    month = {Feb},
    year = {2016},
    url = {http://www.mitls.org/downloads/transcript-collisions.pdf}
    }
  • K. Bhargavan, C. Brzuska, C. Fournet, M. Green, M. Kohlweiss, and S. Zanella-Béguelin, “Downgrade resilience in key-exchange protocols,” in Ieee symposium on security & privacy (oakland), 2016.
    [Bibtex]
    @inproceedings{BhargavanBFGKZ16,
    title = {Downgrade Resilience in Key-Exchange Protocols},
    booktitle = {IEEE Symposium on Security \& Privacy (Oakland)},
    year = 2016,
    author = {Karthikeyan Bhargavan and
    Christina Brzuska and C\'{e}dric Fournet and Matthew Green and Markulf Kohlweiss and Santiago Zanella-B\'{e}guelin},
    organization = {IEEE}
    }
  • J. K. Zinzindohoue, E. Bartzia, and K. Bhargavan, “A verified extensible library of elliptic curves,” in Ieee computer security foundations symposium (csf), 2016.
    [Bibtex]
    @inproceedings{ZBB16,
    author = {Jean Karim Zinzindohoue and Evmorfia-Iro Bartzia and Karthikeyan Bhargavan},
    title = {A Verified Extensible Library of Elliptic Curves},
    booktitle = {IEEE Computer Security Foundations Symposium (CSF)},
    optpages = {},
    year = {2016}
    }
  • H. Halpin and G. Steel, Security guidelines for cryptographic algorithms in the w3c web cryptography api, 2016.
    [Bibtex]
    @misc{halpin:cfrg-webcrypto,
    author = {Harry Halpin and Graham Steel},
    title = {Security Guidelines for Cryptographic Algorithms in the W3C Web Cryptography API},
    howpublished = {IRTF CryptoForum Research Group},
    url = {https://datatracker.ietf.org/doc/draft-irtf-cfrg-webcrypto-algorithms},
    year = {2016},
    month = may
    }
  • [PDF] K. Bhargavan and G. Leurent, “On the Practical (In-)Security of 64-bit Block Ciphers,” in Acm conference on computer and communications security (ccs’16), 2016.
    [Bibtex]
    @inproceedings{BL16:Sweet32,
    author = {Karthikeyan Bhargavan and Ga\"{e}tan Leurent},
    title = {{On the Practical (In-)Security of 64-bit Block Ciphers}},
    booktitle = {ACM Conference on Computer and Communications Security (CCS'16)},
    year = 2016,
    pdf = {pubs/sweet32-on-the-practical-insecurity-ccs16.pdf},
    url = {pubs/sweet32-on-the-practical-insecurity-ccs16.pdf}
    }
  • K. Bhargavan, C. Fournet, and M. Kohlweiss, “miTLS: Verifying Protocol Implementations against Real-World Attacks,” Ieee security & privacy magazine, vol. 14, iss. 6, pp. 18-25, 2016.
    [Bibtex]
    @article{7782710,
    author = {K. Bhargavan and C. Fournet and M. Kohlweiss},
    journal = {IEEE Security \& Privacy Magazine},
    title = {{miTLS: Verifying Protocol Implementations against Real-World Attacks}},
    year = {2016},
    volume = {14},
    number = {6},
    pages = {18-25}
    }
  • K. Bhargavan, A. D. -, C. Fournet, A. Gollamudi, G. Gonthier, N. Kobeissi, N. Kulatova, A. Rastogi, T. S. -, N. Swamy, and S. Z. Béguelin, “Formal verification of smart contracts: short paper,” in ACM workshop on programming languages and analysis for security (plas), 2016, p. 91–96.
    [Bibtex]
    @inproceedings{DBLP:conf/ccs/BhargavanDFGGKK16,
    author = {Karthikeyan Bhargavan and Antoine Delignat{-}Lavaud and C{\'{e}}dric Fournet and Anitha Gollamudi and Georges Gonthier and Nadim Kobeissi and Natalia Kulatova and Aseem Rastogi and Thomas Sibut{-}Pinote and Nikhil Swamy and Santiago Zanella B{\'{e}}guelin},
    title = {Formal Verification of Smart Contracts: Short Paper},
    booktitle = {{ACM} Workshop on Programming Languages and Analysis for Security (PLAS)},
    pages = {91--96},
    year = {2016}
    }

2015

  • Y. Juglaret, C. Hritcu, A. Azevedo de Amorim, B. C. Pierce, A. Spector-Zabusky, and A. Tolmach, Towards a fully abstract compiler using Micro-Policies: secure compilation for mutually distrustful components, 2015.
    [Bibtex]
    @misc{yannis-report,
    author = {Yannis Juglaret and
    Catalin Hritcu and
    Arthur {Azevedo de Amorim} and
    Benjamin C. Pierce and
    Antal Spector-Zabusky and
    Andrew Tolmach},
    title = {Towards a Fully Abstract Compiler Using {Micro-Policies}:
    Secure Compilation for Mutually Distrustful Components},
    howpublished = {Technical Report, arXiv:1510.00697},
    url = {http://arxiv.org/abs/1510.00697},
    year = {2015},
    month = oct
    }
  • Z. Paraskevopoulou, C. Hritcu, M. Dénès, L. Lampropoulos, and B. C. Pierce, “Foundational property-based testing,” in 6th international conference on interactive theorem proving (itp), 2015, p. 325–343.
    [Bibtex]
    @inproceedings{Paraskevopoulou15,
    author = {Zoe Paraskevopoulou and
    Catalin Hritcu and
    Maxime D{\'{e}}n{\`{e}}s and
    Leonidas Lampropoulos and
    Benjamin C. Pierce},
    title = {Foundational Property-Based Testing},
    booktitle = {6th International Conference on Interactive Theorem Proving (ITP)},
    shortbooktitle = {ITP},
    pages = {325--343},
    year = {2015},
    ee = {http://dx.doi.org/10.1007/978-3-319-22102-1_22},
    biburl = {http://dblp.uni-trier.de/rec/bib/conf/itp/Paraskevopoulou15},
    url = {http://prosecco.gforge.inria.fr/personal/hritcu/publications/foundational-pbt.pdf},
    editor = {Christian Urban and
    Xingyuan Zhang},
    series = {Lecture Notes in Computer Science},
    volume = {9236},
    publisher = {Springer},
    isbn = {978-3-319-22101-4}
    }
  • [PDF] M. Paiola and B. Blanchet, “From the applied pi calculus to Horn clauses for protocols with lists,” {Inria}, Research Report RR-8823, 2015.
    [Bibtex]
    @techreport{paiola:hal-01239290,
    title = {From the Applied Pi Calculus to {H}orn Clauses for Protocols with Lists},
    author = {Paiola, Miriam and Blanchet, Bruno},
    url = {https://hal.inria.fr/hal-01239290},
    type = {Research Report},
    number = {RR-8823},
    pages = {45},
    institution = {{Inria}},
    year = {2015},
    month = Dec,
    pdf = {https://hal.inria.fr/hal-01239290/file/RR-8823.pdf},
    hal_id = {hal-01239290},
    hal_version = {v1},
    abstract = {Recently, we presented an automatic technique for proving secrecy and authentication properties for security protocols that manipulate lists of unbounded length, for an unbounded number of sessions. That work relies on an extension of Horn clauses, generalized Horn clauses, designed to support unbounded lists, and on a resolution algorithm on these clauses. However, in that previous work, we had to model protocols manually with generalized Horn clauses, which is unpractical.
    In this work, we present an extension of the input language of ProVerif, a variant of the applied pi calculus, to model protocols with lists of unbounded length. We give its formal meaning, translate it automatically to generalized Horn clauses, and prove that this translation is sound.}
    }
  • T. Chothia, B. Smyth, and C. Staite, “Automatically checking commitment protocols in ProVerif without false attacks,” in Post’15: 4th conference on principles of security and trust, 2015, p. 137–155.
    [Bibtex]
    @inproceedings{2015-automated-verification-of-secrecy-using-phases,
    author = {Tom Chothia and Ben Smyth and Chris Staite},
    title = {Automatically Checking Commitment Protocols in {ProVerif} without False Attacks},
    year = {2015},
    booktitle = {POST'15: 4th Conference on Principles of Security and Trust},
    publisher = {Springer},
    series = {LNCS},
    volume = 9036,
    pages = {137--155},
    url = {http://www.bensmyth.com/publications/2015-automated-verification-of-secrecy-using-phases/}
    }
  • U. Dhawan, C. Hritcu, R. Rubin, N. Vasilakis, S. Chiricescu, J. M. Smith, J. Thomas F. {Knight, B. C. Pierce, and A. DeHon, “Architectural support for software-defined metadata processing,” in 20th international conference on architectural support for programming languages and operating systems (asplos), 2015, pp. 487-502.
    [Bibtex]
    @inproceedings{DhawnHRVCSKPD15,
    author = {Udit Dhawan and
    Catalin Hritcu and
    Rafi Rubin and
    Nikos Vasilakis and
    Silviu Chiricescu and
    Jonathan M. Smith and
    Thomas F. {Knight, Jr.} and
    Benjamin C. Pierce and
    Andr\'{e} DeHon},
    title = {Architectural Support for Software-Defined Metadata Processing},
    booktitle = {20th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS)},
    shortbooktitle = {ASPLOS},
    year = {2015},
    month = mar,
    url = {http://ic.ese.upenn.edu/abstracts/sdmp_asplos2015.html},
    pages = {487-502},
    publisher = {ACM}
    }
  • [DOI] A. Azevedo de Amorim, M. Dénès, N. Giannarakis, C. Hritcu, B. C. Pierce, A. Spector-Zabusky, and A. Tolmach, “Micro-Policies: formally verified, tag-based security monitors,” in 36th ieee symposium on security and privacy (oakland s&p), 2015, p. 813–830.
    [Bibtex]
    @inproceedings{AmorimDGHPST15,
    author = { Arthur {Azevedo de Amorim} and
    Maxime D\'en\`es and
    Nick Giannarakis and
    Catalin Hritcu and
    Benjamin C. Pierce and
    Antal {Spector-Zabusky} and
    Andrew Tolmach},
    title = {{Micro-Policies}: Formally Verified, Tag-Based Security Monitors},
    booktitle = {36th IEEE Symposium on Security and Privacy (Oakland S\&P)},
    shortbooktitle = {Oakland S\&P},
    year = {2015},
    month = may,
    url = {http://prosecco.gforge.inria.fr/personal/hritcu/publications/micro-policies.pdf},
    pages = {813--830},
    ee = {http://dx.doi.org/10.1109/SP.2015.55},
    doi = {10.1109/SP.2015.55},
    publisher = {{IEEE} Computer Society},
    isbn = {978-1-4673-6949-7}
    }
  • D. Cadé and B. Blanchet, “Proved generation of implementations from computationally secure protocol specifications,” Journal of computer security, vol. 23, iss. 3, p. 331–402, 2015.
    [Bibtex]
    @article{CadeBlanchetJCS14,
    author = {David Cad{\'e} and Bruno Blanchet},
    title = {Proved Generation of Implementations from Computationally Secure Protocol Specifications},
    journal = {Journal of Computer Security},
    year = 2015,
    volume = 23,
    number = 3,
    pages = {331--402},
    abstract = {In order to obtain implementations of security protocols proved secure
    in the computational model, we previously proposed the following approach:
    we write a specification of the protocol in the input language of
    the computational protocol verifier CryptoVerif, prove it secure using
    CryptoVerif, then generate an OCaml implementation of the protocol from
    the CryptoVerif specification using a specific compiler that we have
    implemented.
    However, until now, this compiler was
    not proved correct, so we did not have real guarantees on the
    generated implementation. In this paper, we fill this gap. We prove
    that this compiler preserves the security properties proved by
    CryptoVerif: if an adversary has probability $p$ of breaking a
    security property in the generated code, then there exists an adversary
    that breaks the property with the same probability $p$ in the
    CryptoVerif specification. Therefore, if the protocol specification
    is proved secure in the computational model by CryptoVerif, then the
    generated implementation is also secure.}
    }
  • A. Delignat-Lavaud and K. Bhargavan, “Network-based origin confusion attacks against HTTPS virtual hosting,” in Proceedings of the 24th international conference on world wide web, 2015, p. 227–237.
    [Bibtex]
    @inproceedings{DelignatBWWW15,
    author = {Delignat-Lavaud, Antoine and Bhargavan, Karthikeyan},
    title = {Network-based Origin Confusion Attacks against {HTTPS} Virtual Hosting},
    booktitle = {Proceedings of the 24th International Conference on World Wide Web},
    series = {WWW '15},
    year = {2015},
    publisher = {ACM},
    location = {Florence, Italy},
    pages = {227--237}
    }
  • K. Bhargavan, A. Delignat-Lavaud, and A. Pironti, “Verified contributive channel bindings for compound authentication,” in Proceedings of the ISOC network and distributed system security symposium (NDSS ’15), 2015.
    [Bibtex]
    @inproceedings{BhargavanDP15,
    author = {Karthikeyan Bhargavan and Antoine Delignat-Lavaud and Alfredo Pironti},
    title = {Verified Contributive Channel Bindings for Compound Authentication},
    booktitle = {Proceedings of the {ISOC} Network and Distributed System Security Symposium ({NDSS} '15)},
    month = {Feb},
    year = {2015},
    url = {http://antoine.delignat-lavaud.fr/doc/ndss15.pdf}
    }
  • B. Beurdouche, K. Bhargavan, A. Delignat-Lavaud, C. Fournet, M. Kohlweiss, A. Pironti, P. Strub, and J. K. Zinzindohoue, “A messy state of the union: taming the composite state machines of tls,” in Ieee symposium on security & privacy (oakland), 2015.
    [Bibtex]
    @inproceedings{BhargavanDFPS15,
    title = {A Messy State of the Union: Taming the Composite State Machines of TLS},
    booktitle = {IEEE Symposium on Security \& Privacy (Oakland)},
    year = 2015,
    author = {Benjamin Beurdouche and
    Karthikeyan Bhargavan and
    Antoine Delignat-Lavaud and
    C{\'e}dric Fournet and
    Markulf Kohlweiss and
    Alfredo Pironti and
    Pierre-Yves Strub and
    Jean Karim Zinzindohoue},
    organization = {IEEE}
    }
  • B. Beurdouche, A. Delignat-Lavaud, N. Kobeissi, A. Pironti, and K. Bhargavan, “FLEXTLS: A Tool for Testing TLS Implementations,” in Woot’15: 9th usenix workshop on offensive technologies, 2015.
    [Bibtex]
    @inproceedings{2015-flextls,
    author = {Benjamin Beurdouche and Antoine Delignat-Lavaud and Nadim Kobeissi and Alfredo Pironti and Karthikeyan Bhargavan},
    title = {{FLEXTLS: A Tool for Testing TLS Implementations}},
    year = {2015},
    booktitle = {WOOT'15: 9th USENIX Workshop on Offensive Technologies},
    publisher = {USENIX Association}
    }
  • D. Adrian, K. Bhargavan, Z. Durumeric, P. Gaudry, M. Green, A. J. Halderman, N. Heninger, D. Springall, E. Thomé, L. Valenta, B. VanderSloot, E. Wustrow, S. Zanella-Béguelin, and P. and Zimmermann, “Imperfect forward secrecy: how diffie-hellman fails in practice,” in Acm conference on computer and communications security (ccs’15), 2015, p. 5–17.
    [Bibtex]
    @inproceedings{2015-logjam,
    author = {David Adrian and Karthikeyan Bhargavan and Zakir Durumeric and Pierrick Gaudry and Matthew Green and J. Alex Halderman and Nadia Heninger and Drew Springall and Emmanuel Thom\'{e} and Luke Valenta and Benjamin VanderSloot and Eric Wustrow and Santiago Zanella-B\'{e}guelin and and Paul Zimmermann},
    title = {Imperfect Forward Secrecy: How Diffie-Hellman Fails in Practice},
    booktitle = {ACM Conference on Computer and Communications Security (CCS'15)},
    year = {2015},
    pages = {5--17}
    }

2014

  • G. Bana and H. Comon-Lundh, “A computationally complete symbolic attacker for equivalence properties,” in Acm conference on computer and communications security (ccs’14), New York, NY, USA, 2014, p. 609–620.
    [Bibtex]
    @inproceedings{BanComCCS14,
    author = {Bana, Gergei and Comon-Lundh, Hubert},
    title = {A Computationally Complete Symbolic Attacker for Equivalence Properties},
    booktitle = {ACM Conference on Computer and Communications Security (CCS'14)},
    year = {2014},
    month = {Nov},
    pages = {609--620},
    publisher = {ACM},
    address = {New York, NY, USA},
    keywords = {computational soundness, protocol indistinguishability, security protocols, symbolic verification},
    abstract = {We consider the problem of computational indistinguishability of protocols.
    We design a symbolic model, amenable to automated deduction, such that a successful inconsistency proof implies computational indistinguishability. Conversely, symbolic models of distinguishability provide clues for likely computational attacks. We follow the idea
    we introduced earlier for reachability properties, axiomatizing what an attacker cannot violate. This results a computationally complete symbolic attacker, and ensures unconditional computational soundness for the symbolic analysis. We present a small library of computationally sound, modular axioms, and test our technique on an example protocol. Despite additional difficulties stemming from the equivalence properties, the models and the soundness proofs turn out to be simpler than they were for reachability properties.}
    }
  • G. Bana, K. Hasebe, and M. Okada, “Computationally complete symbolic adversary and key exchange (in japanese),” in Proceedings of the 31st symposium on cryptography and information security, CD-ROM (3C5-3), 2014.
    [Bibtex]
    @conference{BanaHaseOkaCSIS14,
    author = {Bana, Gergei and Hasebe, Koji and Okada, Mitsuhiro},
    title = {Computationally Complete Symbolic Adversary and Key Exchange (in Japanese)},
    booktitle = {Proceedings of The 31st Symposium on Cryptography and Information Security},
    year = {2014},
    month = {Jan},
    address = {CD-ROM (3C5-3)}
    }
  • B. Smyth and D. Bernhard, “Ballot secrecy and ballot independence: definitions and relations,” Cryptology ePrint Archive, 2013/235, 2014.
    [Bibtex]
    @techreport{2014-ballot-independence-for-election-schemes,
    author = {Ben Smyth and David Bernhard},
    title = {{Ballot secrecy and ballot independence: definitions and relations}},
    year = {2014},
    institution = {Cryptology ePrint Archive},
    number = {2013/235},
    url = {http://bensmyth.com/publications/2014-ballot-independence-for-election-schemes/}
    }
  • B. Smyth and D. Bernhard, “Ballot secrecy with malicious bulletin boards,” Cryptology ePrint Archive, 2014/822, 2014.
    [Bibtex]
    @techreport{2014-ballot-secrecy,
    author = {Ben Smyth and David Bernhard},
    title = {{Ballot secrecy with malicious bulletin boards}},
    year = {2014},
    institution = {Cryptology ePrint Archive},
    number = {2014/822},
    url = {http://bensmyth.com/publications/2014-ballot-secrecy/}
    }
  • B. Smyth, S. Frink, and M. R. Clarkson, Election Verifiability: Definitions and an Analysis of Helios and JCJ, 2014.
    [Bibtex]
    @unpublished{2014-election-verifiability,
    author = {Ben Smyth and Steven Frink and Michael R. Clarkson},
    title = {{Election Verifiability: Definitions and an Analysis of Helios and JCJ}},
    year = {2014},
    url = {http://bensmyth.com/publications/2014-election-verifiability/}
    }
  • A. McCarthy, B. Smyth, and E. A. Quaglia, “Hawk and Aucitas: e-auction schemes from the Helios and Civitas e-voting schemes,” in Fc’14: 18th international conference on financial cryptography and data security, 2014.
    [Bibtex]
    @inproceedings{2014-Hawk-and-Aucitas-auction-schemes,
    author = {Adam McCarthy and Ben Smyth and Elizabeth A. Quaglia},
    title = {{Hawk and Aucitas: e-auction schemes from the Helios and Civitas e-voting schemes}},
    year = {2014},
    booktitle = {FC'14: 18th International Conference on Financial Cryptography and Data Security},
    publisher = spv,
    series = lncs,
    volume = {8437},
    url = {http://bensmyth.com/publications/2014-Hawk-and-Aucitas-auction-schemes/}
    }
  • B. Blanchet, “Automatic verification of security protocols in the symbolic model: the verifier ProVerif,” in Foundations of security analysis and design vii, fosad tutorial lectures, A. Aldini, J. Lopez, and F. Martinelli, Eds., Springer verlag, 2014, vol. 8604, p. 54–87.
    [Bibtex]
    @incollection{BlanchetFOSAD14,
    author = {Bruno Blanchet},
    title = {Automatic Verification of Security Protocols in the Symbolic Model: the Verifier {P}ro{V}erif},
    booktitle = {Foundations of Security Analysis and Design VII, FOSAD Tutorial Lectures},
    pages = {54--87},
    publisher = spv,
    year = {2014},
    editor = {Alessandro Aldini and Javier Lopez and Fabio Martinelli},
    volume = {8604},
    series = lncs,
    abstract = {After giving general context on the verification of security
    protocols, we focus on the automatic symbolic protocol verifier
    ProVerif. This verifier can prove secrecy, authentication, and
    observational equivalence properties of security protocols, for an
    unbounded number of sessions of the protocol. It supports a wide range
    of cryptographic primitives defined by rewrite rules or by equations.
    The tool takes as input a description of the protocol to verify in a
    process calculus, an extension of the pi calculus with
    cryptography. It automatically translates this protocol into an abstract
    representation of the protocol by Horn clauses, and determines whether
    the desired security properties hold by resolution on these clauses.}
    }
  • K. Bhargavan, A. Delignat-Lavaud, and S. Maffeis, “Defensive JavaScript – Building and Verifying Secure Web Components,” in Foundations of security analysis and design vii, fosad tutorial lectures, A. Aldini, J. Lopez, and F. Martinelli, Eds., Springer verlag, 2014, vol. 8604, pp. 88-123.
    [Bibtex]
    @incollection{BhargavanFOSAD14,
    author = {Karthikeyan Bhargavan and
    Antoine Delignat-Lavaud and
    Sergio Maffeis},
    title = {{Defensive JavaScript - Building and Verifying Secure Web
    Components}},
    booktitle = {Foundations of Security Analysis and Design VII, FOSAD Tutorial Lectures},
    year = {2014},
    pages = {88-123},
    publisher = spv,
    editor = {Alessandro Aldini and Javier Lopez and Fabio Martinelli},
    volume = {8604},
    series = lncs
    }
  • M. Paiola, “Verification of cryptographic protocols with lists of unbounded length,” PhD Thesis, 2014.
    [Bibtex]
    @phdthesis{Paiola14,
    author = {Miriam Paiola},
    title = {Verification of cryptographic protocols with lists of unbounded length},
    school = {Universit{\'e} Paris VII},
    year = 2014,
    month = may
    }
  • [DOI] M. Backes, C. Hritcu, and M. Maffei, “Union, intersection, and refinement types and reasoning about type disjointness for secure protocol implementations,” Journal of computer security (jcs); special issue on foundational aspects of security, vol. 22, iss. 2, p. 301–353, 2014.
    [Bibtex]
    @article{Backes:Hritcu:Maffei:14jcs,
    author = {Michael Backes and
    Catalin Hritcu and
    Matteo Maffei},
    title = {Union, Intersection, and Refinement Types and Reasoning About Type Disjointness for Secure Protocol Implementations},
    journal = {Journal of Computer Security (JCS); Special Issue on Foundational Aspects of Security},
    volume = {22},
    number = {2},
    pages = {301--353},
    publisher = {IOS Press},
    month = feb,
    year = 2014,
    doi = {10.3233/JCS-130493},
    ee = {http://iospress.metapress.com/content/G0531100122U1K6K},
    url = {http://prosecco.gforge.inria.fr/personal/hritcu/publications/rcf-and-or-coq-jcs2014.pdf},
    abstract = {We present a new type system for verifying the security of reference
    implementations of cryptographic protocols written in a core
    functional programming language. The type system combines prior work
    on refinement types, with union, intersection, and polymorphic types,
    and with the novel ability to reason statically about the disjointness
    of types. The increased expressivity enables the analysis of
    important protocol classes that were previously out of scope for the
    type-based analyses of reference protocol implementations. In
    particular, our types can statically characterize: (i) more usages of
    asymmetric cryptography, such as signatures of private data and
    encryptions of authenticated data; (ii) authenticity and integrity
    properties achieved by showing knowledge of secret data; (iii)
    applications based on zero-knowledge proofs. The type system comes
    with a mechanized proof of correctness and an efficient type-checker.}
    }
  • A. Azevedo de Amorim, N. Collins, A. DeHon, D. Demange, C. Hritcu, D. Pichardie, B. C. Pierce, R. Pollack, and A. Tolmach, “A verified information-flow architecture,” in 41st acm sigplan-sigact symposium on principles of programming languages (popl), 2014, pp. 165-178.
    [Bibtex]
    @inproceedings{AmorimCDDHPPPT14,
    title = {A Verified Information-Flow Architecture},
    author = {
    Arthur {Azevedo de Amorim} and
    Nathan Collins and
    Andr\'e DeHon and
    Delphine Demange and
    Catalin Hritcu and
    David Pichardie and
    Benjamin C. Pierce and
    Randy Pollack and
    Andrew Tolmach
    },
    booktitle = {41st ACM SIGPLAN-SIGACT Symposium on Principles
    of Programming Languages (POPL)},
    shortbooktitle = {POPL},
    month = jan,
    year = {2014},
    publisher = {ACM},
    pages = {165-178},
    isbn = {978-1-4503-2544-8},
    ee = {http://doi.acm.org/10.1145/2535838.2535839},
    url = {http://www.crash-safe.org/node/29},
    abstract = {SAFE is a clean-slate design for a highly secure computer
    system, with pervasive mechanisms for tracking and limiting
    information flows. At the lowest level, the SAFE hardware supports
    fine-grained programmable tags, with efficient and flexible
    propagation and combination of tags as instructions are executed.
    The operating system virtualizes these generic facilities to present
    an information-flow abstract machine that allows user programs to
    label sensitive data with rich confidentiality policies. We present
    a formal, machine-checked model of the key hardware and software
    mechanisms used to control information flow in SAFE and
    an end-to-end proof of noninterference for this model.}
    }
  • N. Swamy, C. Fournet, A. Rastogi, K. Bhargavan, J. Chen, P. Strub, and G. M. Bierman, “Gradual typing embedded securely in javascript,” in 41st acm sigplan-sigact symposium on principles of programming languages (popl), 2014, pp. 425-438.
    [Bibtex]
    @inproceedings{SwamyFRBCSB14,
    author = {Nikhil Swamy and
    C{\'e}dric Fournet and
    Aseem Rastogi and
    Karthikeyan Bhargavan and
    Juan Chen and
    Pierre-Yves Strub and
    Gavin M. Bierman},
    title = {Gradual typing embedded securely in JavaScript},
    booktitle = {41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)},
    year = {2014},
    pages = {425-438},
    url = {http://prosecco.inria.fr/personal/karthik/pubs/tsstar-popl14.pdf}
    }
  • [PDF] K. Bhargavan, A. Delignat-Lavaud, C. Fournet, A. and Pironti, and P. Strub, “Triple handshakes and cookie cutters: breaking and fixing authentication over tls,” in Ieee symposium on security & privacy (oakland), 2014.
    [Bibtex]
    @inproceedings{BhargavanDFPS14,
    title = {Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication over TLS},
    booktitle = {IEEE Symposium on Security \& Privacy (Oakland)},
    year = 2014,
    url = {pubs/triple-handshakes-and-cookie-cutters-sp14.pdf},
    pdf = {pubs/triple-handshakes-and-cookie-cutters-sp14.pdf},
    author = {Karthikeyan Bhargavan and Antoine Delignat-Lavaud and C{\'e}dric Fournet and and Alfredo Pironti and Pierre-Yves Strub}
    }
  • C. Bansal, K. Bhargavan, A. Delignat-Lavaud, and S. Maffeis, “Discovering concrete attacks on website authorization by formal analysis,” Journal of computer security, vol. 22, iss. 4, p. 601–657, 2014.
    [Bibtex]
    @article{BansalBDM14,
    author = {Chetan Bansal and Karthikeyan Bhargavan and Antoine Delignat-Lavaud and Sergio Maffeis},
    title = {Discovering concrete attacks on website authorization by formal analysis},
    journal = {Journal of Computer Security},
    year = 2014,
    volume = 22,
    number = 4,
    pages = {601--657},
    month = apr
    }
  • K. Bhargavan, C. Fournet, M. Kohlweiss, A. Pironti, P. Strub, and S. Zanella-Béguelin, “Proving the tls handshake secure (as it is),” in Proceedings of crypto, 2014.
    [Bibtex]
    @inproceedings{HandshakeCrypto14,
    author = {Karthikeyan Bhargavan and C\'{e}dric Fournet and Markulf Kohlweiss and Alfredo Pironti and Pierre-Yves Strub and Santiago Zanella-B\'{e}guelin},
    title = {Proving the TLS Handshake Secure (as it is)},
    booktitle = {Proceedings of CRYPTO},
    year = {2014},
    note = {Long version at Cryptology ePrint Archive, Report 2014/182: \url{https://eprint.iacr.org/2014/182}}
    }
  • A. Delignat-Lavaud, M. Abadí, M. Birrell, I. Mironov, T. Wobber, and Y. Xie, “Web PKI: closing the gap between guidelines and practices,” in Proceedings of the ISOC network and distributed system security symposium (NDSS ’14), 2014.
    [Bibtex]
    @inproceedings{DelignatABMWX14,
    author = {Antoine Delignat-Lavaud and Martin Abad\'i and Matthew Birrell and Ilya Mironov and Ted Wobber and Yinglian Xie},
    title = {Web {PKI}: Closing the Gap between Guidelines and Practices},
    booktitle = {Proceedings of the {ISOC} Network and Distributed System Security Symposium ({NDSS} '14)},
    month = {Feb},
    year = {2014},
    url = {http://antoine.delignat-lavaud.fr/doc/ndss14.pdf}
    }
  • S. Kremer and R. Künnemann, “Automated analysis of security protocols with global state,” in Ieee symposium on security & privacy (oakland), 2014.
    [Bibtex]
    @inproceedings{DBLP:journals/corr/KremerK14,
    author = {Steve Kremer and
    Robert K{\"u}nnemann},
    title = {Automated analysis of security protocols with global state},
    booktitle = {IEEE Symposium on Security \& Privacy (Oakland)},
    year = 2014
    }
  • E. Bartzia and P. Strub, “A formal library for elliptic curves in the coq proof assistant,” in Interactive theorem proving (itp), 2014, pp. 77-92.
    [Bibtex]
    @inproceedings{DBLP:conf/itp/BartziaS14,
    author = {Evmorfia-Iro Bartzia and
    Pierre-Yves Strub},
    title = {A Formal Library for Elliptic Curves in the Coq Proof Assistant},
    booktitle = {Interactive Theorem Proving (ITP)},
    year = {2014},
    pages = {77-92}
    }
  • T. Gauthier, C. Kaliszyk, C. Keller, and M. Norrish, “Beagle as a HOL4 external ATP method,” in Paar-2014 – 4th workshop on practical aspects of automated reasoning, 2014, p. 50–59.
    [Bibtex]
    @inproceedings{conf/paar/GauthierKKN14,
    author = {Thibault Gauthier and
    Cezary Kaliszyk and
    Chantal Keller and
    Michael Norrish},
    title = {Beagle as a {HOL4} external {ATP} method},
    booktitle = {PAAR-2014 - 4th Workshop on Practical Aspects of Automated Reasoning},
    year = 2014,
    series = {EPiC Series in Computing},
    volume = 31,
    publisher = {EasyChair},
    month = jul,
    pages = {50--59}
    }
  • V. Cortier and G. Steel, “A Generic Security API for Symmetric Key Management on Cryptographic Devices,” Information and Computation, vol. 238, p. 25, 2014.
    [Bibtex]
    @article{cortier:hal-00881072,
    title = {{A Generic Security API for Symmetric Key Management on Cryptographic Devices}},
    author = {Cortier, V{\'e}ronique and Steel, Graham},
    url = {https://hal.inria.fr/hal-00881072},
    journal = {{Information and Computation}},
    publisher = {{Elsevier}},
    volume = {238},
    number = {0},
    pages = {25},
    year = {2014},
    hal_id = {hal-00881072},
    hal_version = {v1}
    }

2013

  • G. Bana, P. Adaõ, and H. Sakurada, “Computationally complete symbolic adversary and computationally sound veri?cation of security protocols (in japanese),” in Proceedings of the 30th symposium on cryptography and information security, CD-ROM (4D1-3), 2013.
    [Bibtex]
    @conference{BanaAdaoSakuCSIS13,
    author = {Bana, Gergei and Ada\~o, Pedro and Sakurada, Hideki},
    title = {Computationally Complete Symbolic Adversary and Computationally Sound Veri?cation of Security Protocols (in Japanese)},
    booktitle = {Proceedings of The 30th Symposium on Cryptography and Information Security},
    year = {2013},
    month = {Jan},
    address = {CD-ROM (4D1-3)}
    }
  • D. Cadé, “Proved implementations of cryptographic protocols in the computational model,” PhD Thesis, 2013.
    [Bibtex]
    @phdthesis{Cade13c,
    author = {David Cad{\'e}},
    title = {Proved Implementations of Cryptographic Protocols
    in the Computational Model},
    school = {Universit{\'e} Paris VII},
    year = 2013,
    month = dec
    }
  • G. Bana, K. Hasebe, and M. Okada, “Computationally complete symbolic attacker and key exchange,” in Acm conference on computer and communications security (ccs’13), Berlin, Germany, 2013, p. 1231–1246.
    [Bibtex]
    @inproceedings{BanaHasebeOkadaCCS2013,
    author = {Gergei Bana and Koji Hasebe and Mitsuhiro Okada},
    title = {Computationally Complete Symbolic Attacker and Key Exchange},
    booktitle = {ACM Conference on Computer and Communications Security (CCS'13)},
    pages = {1231--1246},
    year = 2013,
    address = {Berlin, Germany},
    month = nov,
    publisher = {ACM},
    abstract = {Recently, Bana and Comon-Lundh introduced the notion of computationally complete symbolic attacker to deliver unconditional computational soundness to symbolic protocol verification. First we explain the relationship between their technique and Fitting's embedding of classical logic into S4. Then, based on predicates for ``key usability'', we provide an axiomatic system in their framework to handle secure encryption when keys are allowed to be sent. We examine both IND-CCA2 and KDM-CCA2 encryptions, both symmetric and asymmetric situations. For unforgeability, we consider INT-CTXT encryptions. This technique does not require the usual limitations of computational soundness such as the absence of dynamic corruption, the absence of key-cycles or unambiguous parsing of bit strings. In particular, if a key-cycle possibly corrupts CCA2 encryption, our technique delivers an attack. If it does not endanger security, the security proof goes through. We illustrate how our notions can be applied in protocol proofs.}
    }
  • B. Blanchet and M. Paiola, “Automatic verification of protocols with lists of unbounded length,” in Acm conference on computer and communications security (ccs’13), Berlin, Germany, 2013, p. 573–584.
    [Bibtex]
    @inproceedings{BlanchetPaiolaCCS13,
    author = {Bruno Blanchet and Miriam Paiola},
    title = {Automatic Verification of Protocols with Lists of Unbounded Length},
    booktitle = {ACM Conference on Computer and Communications Security (CCS'13)},
    pages = {573--584},
    year = 2013,
    address = {Berlin, Germany},
    month = nov,
    publisher = {ACM},
    url = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetPaiolaCCS13.html},
    abstract = {We present a novel automatic technique for proving secrecy and authentication properties for
    security protocols that manipulate lists of unbounded length, for
    an unbounded number of sessions. This result is achieved by extending the Horn clause approach of the automatic protocol verifier ProVerif. We extend the Horn clauses to be able to represent lists of unbounded length. We adapt the resolution algorithm to handle the new class of Horn clauses, and prove the soundness of this new algorithm.
    We have implemented our algorithm and successfully tested it on several protocol examples, including XML protocols coming from web services.}
    }
  • M. Paiola and B. Blanchet, “Verification of security protocols with lists: from length one to unbounded length,” Journal of computer security, vol. 21, iss. 6, p. 781–816, 2013.
    [Bibtex]
    @article{PaiolaBlanchetJCS13,
    author = {Miriam Paiola and Bruno Blanchet},
    title = {Verification of Security Protocols with Lists:
    from Length One to Unbounded Length},
    journal = {Journal of Computer Security},
    year = 2013,
    volume = 21,
    number = 6,
    pages = {781--816},
    month = dec,
    note = {Special issue POST'12},
    url = {https://bblanche.gitlabpages.inria.fr/publications/PaiolaBlanchetJCS13.html},
    abstract = {We present a novel, simple technique for proving secrecy properties for
    security protocols that manipulate lists of unbounded length, for
    an unbounded number of sessions.
    More specifically, our technique relies on the Horn clause
    approach used in the automatic verifier ProVerif: we show that if
    a protocol is proven secure by our technique with lists of length
    one, then it is secure for lists of unbounded length.
    Interestingly, this theorem relies on approximations made by our
    verification technique: in general, secrecy for lists of length
    one does not imply secrecy for lists of unbounded length.
    Our result can be used in particular to prove secrecy properties
    for group protocols with an unbounded number of participants and
    for some XML protocols (web services) with ProVerif.}
    }
  • B. Smyth and D. Bernhard, “Ballot secrecy and ballot independence coincide,” in Esorics’13: 18th european symposium on research in computer security, 2013, pp. 463-480.
    [Bibtex]
    @inproceedings{2013-ballot-independence-for-election-schemes,
    author = {Ben Smyth and David Bernhard},
    title = {{Ballot secrecy and ballot independence coincide}},
    year = {2013},
    booktitle = {ESORICS'13: 18th European Symposium on Research in Computer Security},
    publisher = {Springer},
    series = {LNCS},
    pages = {463-480},
    volume = {8134},
    url = {http://www.bensmyth.com/publications/2013-ballot-independence-for-election-schemes/},
    abstract = {We study ballot independence for election schemes. First, we formally define ballot independence as a cryptographic game and prove that ballot secrecy implies ballot independence. Secondly, we introduce a notion of controlled malleability and show that it is sufficient for ballot independence. We also show that non-malleable ballots are sufficient, but not necessary, for ballot independence. Thirdly, we prove that ballot independence is sufficient for ballot secrecy under practical assumptions.
    Our results show that ballot independence is necessary in election schemes satisfying ballot secrecy. Furthermore, our sufficient conditions will enable simpler proofs of ballot secrecy.},
    x-language = {EN},
    x-audience = {international},
    x-town = {Egham},
    x-country = {GB}
    }
  • B. Smyth and A. Pironti, “Truncating TLS Connections to Violate Beliefs in Web Applications,” in Woot’13: 7th usenix workshop on offensive technologies, 2013.
    [Bibtex]
    @inproceedings{2013-truncation-attacks-to-violate-beliefs,
    author = {Ben Smyth and Alfredo Pironti},
    title = {{Truncating TLS Connections to Violate Beliefs in Web Applications}},
    year = {2013},
    booktitle = {WOOT'13: 7th USENIX Workshop on Offensive Technologies},
    publisher = {USENIX Association},
    note = {First appeared at Black Hat USA 2013.},
    url = {http://www.bensmyth.com/publications/2013-truncation-attacks-to-violate-beliefs/},
    abstract = {We identify logical web application flaws which can be exploited by TLS truncation attacks to desynchronize the user- and server-perspective of an application's state. It follows immediately that servers may make false assumptions about users, hence, the flaw constitutes a security vulnerability. Moreover, in the context of authentication systems, we exploit the vulnerability to launch the following practical attacks: we exploit the Helios electronic voting system to cast votes on behalf of honest voters, take full control of Microsoft Live accounts, and gain temporary access to Google accounts.},
    x-language = {EN},
    x-audience = {international},
    x-town = {Washington},
    x-country = {US}
    }
  • A. Delignat-Lavaud, K. Bhargavan, and S. Maffeis, “Language-based defenses against untrusted browser origins,” in Proceedings of the 22th usenix security symposium, 2013.
    [Bibtex]
    @inproceedings{DelignatBM13,
    author = {Antoine Delignat-Lavaud and Karthikeyan Bhargavan and Sergio Maffeis},
    title = {Language-Based Defenses Against Untrusted Browser Origins},
    booktitle = {Proceedings of the 22th USENIX Security Symposium},
    year = {2013},
    url = {http://prosecco.inria.fr/personal/karthik/pubs/language-based-defenses-against-untrusted-origins-sec13.pdf}
    }
  • K. Bhargavan, C. Fournet, M. Kohlweiss, A. Pironti, and P. Strub, “Implementing tls with verified cryptographic security,” in Ieee symposium on security & privacy (oakland), 2013, pp. 445-462.
    [Bibtex]
    @inproceedings{BhargavanFKPS13,
    title = {Implementing TLS with Verified Cryptographic Security},
    abstract = {TLS is possibly the most used protocol for secure communications, with a 18-year history of flaws and fixes, ranging from its protocol logic to its cryptographic design, and from the Internet standard to its diverse implementations.
    We develop a verified reference implementation of TLS 1.2. Our code fully supports its wire formats, ciphersuites, sessions and connections, re-handshakes and resumptions, alerts and errors, and data fragmentation, as prescribed in the RFCs; it interoperates with mainstream web browsers and servers. At the same time, our code is carefully structured to enable its modular, automated verification, from its main API down to computational assumptions on its cryptographic algorithms.
    Our implementation is written in F# and specified in F7. We present security specifications for its main components, such as authenticated stream encryption for the record layer and key establishment for the handshake. We describe their verification using the F7 typechecker. To this end, we equip each cryptographic primitive and construction of TLS with a new typed interface that captures its security properties, and we gradually replace concrete implementations with ideal functionalities. We finally typecheck the protocol state machine, and obtain precise security theorems for TLS, as it is implemented and deployed. We also revisit classic attacks and report a few new ones.},
    x-language = {EN},
    x-audience = {international},
    booktitle = {IEEE Symposium on Security \& Privacy (Oakland)},
    x-town = {San Francisco},
    x-country = {US},
    year = 2013,
    pages = {445-462},
    author = {Karthikeyan Bhargavan and C{\'e}dric Fournet and Markulf Kohlweiss and Alfredo Pironti and Pierre-Yves Strub},
    url = {http://prosecco.inria.fr/personal/karthik/pubs/implementing-tls-with-verified-cryptographic-security-sp13.pdf}
    }
  • D. Cadé and B. Blanchet, “From computationally-proved protocol specifications to implementations and application to SSH,” Journal of wireless mobile networks, ubiquitous computing, and dependable applications (jowua), vol. 4, iss. 1, p. 4–31, 2013.
    [Bibtex]
    @article{CadeBlanchetJoWUA13,
    author = {David Cad{\'e} and Bruno Blanchet},
    title = {From Computationally-Proved Protocol Specifications to Implementations and Application to {SSH}},
    journal = {Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications (JoWUA)},
    year = 2013,
    volume = 4,
    number = 1,
    pages = {4--31},
    month = mar,
    publisher = {Innovative Information Science \& Technology Research Group (ISYOU)},
    abstract = {This paper presents a novel technique for obtaining implementations
    of security protocols, proved secure in the computational model.
    We formally specify the protocol to prove, we prove this specification
    using the computationally-sound protocol verifier CryptoVerif, and
    we automatically translate it into an implementation in
    OCaml using a new compiler that we have implemented.
    We applied this approach to the SSH
    Transport Layer protocol: we proved the authentication of the server and
    the secrecy of the session keys in
    this protocol and verified that the generated implementation successfully
    interacts with OpenSSH. We explain these proofs, as well as an extension
    of CryptoVerif needed for the proof of secrecy of the session keys.
    The secrecy of messages sent over the SSH tunnel
    cannot be proved due to known weaknesses in SSH with CBC-mode
    encryption.},
    x-language = {EN},
    x-audience = {international},
    note = {Special issue ARES'12},
    url = {https://bblanche.gitlabpages.inria.fr/publications/CadeBlanchetJoWUA13.html}
    }
  • [PDF] V. Cortier and B. Smyth, “Attacking and fixing Helios: An analysis of ballot secrecy,” Journal of computer security, vol. 21, iss. 1, p. 89–148, 2013.
    [Bibtex]
    @article{2012-attacking-ballot-secrecy-in-Helios,
    author = {V\'{e}ronique Cortier and Ben Smyth},
    title = {{Attacking and fixing Helios: An analysis of ballot secrecy}},
    journal = {Journal of Computer Security},
    year = {2013},
    volume = {21},
    number = {1},
    pages = {89--148},
    url = {http://www.bensmyth.com/publications/2012-attacking-ballot-secrecy-in-Helios/},
    pdf = {http://www.bensmyth.com/files/Smyth12-attacking-Helios.pdf},
    abstract = {Helios 2.0 is an open-source web-based end-to-end verifiable electronic voting system, suitable for use in low-coercion environments. In this article, we analyse ballot secrecy in Helios and discover a vulnerability which allows an adversary to compromise the privacy of voters. The vulnerability exploits the absence of ballot independence in Helios and works by replaying a voter's ballot or a variant of it, the replayed ballot magnifies the voter's contribution to the election outcome and this magnification can be used to violated privacy. We demonstrate the practicality of the attack by violating a voter's privacy in a mock election using the software implementation of Helios. Moreover, the feasibility of an attack is considered in the context of French legislative elections and, based upon our findings, we believe it constitutes a real threat to ballot secrecy. We present a fix and show that our solution satisfies a formal definition of ballot secrecy using the applied pi calculus. Furthermore, we present similar vulnerabilities in other electronic voting protocols -- namely, the schemes by Lee et al., Sako & Kilian, and Schoenmakers -- which do not assure ballot independence. Finally, we argue that independence and privacy properties are unrelated, and non-malleability is stronger than independence.},
    x-language = {EN},
    x-audience = {international},
    publisher = {IOS Press}
    }
  • C. Bansal, K. Bhargavan, A. Delignat-Lavaud, and S. Maffeis, “Keys to the cloud: formal analysis and concrete attacks on encrypted web storage,” in 2nd conference on principles of security and trust (post 2013), Rome, Italy, 2013, p. 126–146.
    [Bibtex]
    @inproceedings{BansalBDM13,
    author = {Chetan Bansal and Karthikeyan Bhargavan and Antoine Delignat-Lavaud and Sergio Maffeis},
    title = {Keys to the Cloud: Formal Analysis and Concrete Attacks on Encrypted Web Storage},
    booktitle = {2nd Conference on Principles of Security and Trust (POST 2013)},
    pages = {126--146},
    year = 2013,
    editor = {David Basin and John Mitchell},
    volume = 7796,
    series = lncs,
    address = {Rome, Italy},
    month = mar,
    publisher = spv,
    url = {http://prosecco.inria.fr/personal/karthik/pubs/keys-to-the-cloud-post13.pdf}
    }
  • D. Cadé and B. Blanchet, “Proved generation of implementations from computationally-secure protocol specifications,” in 2nd conference on principles of security and trust (post 2013), Rome, Italy, 2013, p. 63–82.
    [Bibtex]
    @inproceedings{CadeBlanchet12b,
    author = {David Cad{\'e} and Bruno Blanchet},
    title = {Proved Generation of Implementations from Computationally-Secure Protocol Specifications},
    booktitle = {2nd Conference on Principles of Security and Trust (POST 2013)},
    pages = {63--82},
    year = 2013,
    editor = {David Basin and John Mitchell},
    volume = 7796,
    series = lncs,
    address = {Rome, Italy},
    month = mar,
    publisher = spv,
    abstract = {In order to obtain implementations of security protocols proved secure
    in the computational model, we have previously implemented a compiler
    that takes a specification of the protocol in the input language of
    the computational protocol verifier CryptoVerif and translates
    it into an OCaml implementation. However, until now, this compiler was
    not proved correct, so we did not have real guarantees on the
    generated implementation. In this paper, we fill this gap. We prove
    that this compiler preserves the security properties proved by
    CryptoVerif: if an adversary has probability p of breaking a
    security property in the generated code, then there exists an adversary
    that breaks the property with the same probability p in the
    CryptoVerif specification. Therefore, if the protocol specification
    is proved secure in the computational model by CryptoVerif, then the
    generated implementation is also secure.},
    x-language = {EN},
    x-audience = {international},
    x-town = {Rome},
    x-country = {IT},
    url = {https://bblanche.gitlabpages.inria.fr/publications/CadeBlanchetPOST13.html}
    }
  • V. Cheval and B. Blanchet, “Proving more observational equivalences with ProVerif,” in 2nd conference on principles of security and trust (post 2013), Rome, Italy, 2013, p. 226–246.
    [Bibtex]
    @inproceedings{ChevalBlanchet12,
    author = {Vincent Cheval and Bruno Blanchet},
    title = {Proving More Observational Equivalences with {P}ro{V}erif},
    booktitle = {2nd Conference on Principles of Security and Trust (POST 2013)},
    pages = {226--246},
    year = 2013,
    editor = {David Basin and John Mitchell},
    volume = 7796,
    series = lncs,
    address = {Rome, Italy},
    month = mar,
    publisher = spv,
    abstract = {This paper presents an extension of the automatic protocol verifier
    ProVerif in order to prove more observational equivalences. ProVerif
    can prove observational equivalence between processes that have the
    same structure but differ by the messages they contain. In order to
    extend the class of equivalences that ProVerif handles, we extend the
    language of terms by defining more functions (destructors) by rewrite
    rules. In particular, we allow rewrite rules with inequalities as
    side-conditions, so that we can express tests ``if then else'' inside
    terms. Finally, we provide an automatic procedure that translates a
    process into an equivalent process that performs as many actions as
    possible inside terms, to allow ProVerif to prove the desired
    equivalence. These extensions have been implemented in ProVerif and
    allow us to automatically prove anonymity in the private
    authentication protocol by Abadi and Fournet.},
    x-language = {EN},
    x-audience = {international},
    x-town = {Rome},
    x-country = {IT},
    url = {https://bblanche.gitlabpages.inria.fr/publications/ChevalBlanchetPOST13.html}
    }
  • [DOI] 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), Egham, U.K., 2013, pp. 327-344.
    [Bibtex]
    @inproceedings{KKS-esorics13,
    address = {Egham, U.K.},
    author = {Kremer, Steve and K{\"u}nnemann, Robert and Steel, Graham},
    booktitle = {{P}roceedings of the 18th {E}uropean {S}ymposium on {R}esearch in {C}omputer {S}ecurity ({ESORICS}'13)},
    editor = {Crampton, Jason and Jajodia, Sushil and Mayes, Keith},
    month = sep,
    publisher = {Springer},
    series = {Lecture Notes in Computer Science},
    title = {Universally Composable Key-Management},
    pages = {327-344},
    volume = {8134},
    year = {2013},
    doi = {10.1007/978-3-642-40203-6_19},
    x-audience = {international},
    x-language = {EN},
    x-town = {Egham},
    x-country = {GB},
    x-yearstart = {2013},
    abstract = {We present the first universally composable key-management functionality, formalized in the GNUC framework by Hofheinz and Shoup. It allows the enforcement of a wide range of security policies and can be extended by diverse key usage operations with no need to repeat the security proof. We illustrate its use by proving an implementation of a security token secure with respect to arbitrary key-usage operations and explore a proof technique that allows the storage of cryptographic keys externally, a novel development in simulation-based security frameworks.}
    }
  • M. J. May and K. Bhargavan, “Towards unified authorization for android,” in 5th international symposium on engineering secure software and systems (essos 2013), 2013, pp. 42-57.
    [Bibtex]
    @inproceedings{MayBhargavan2013,
    author = {Michael J. May and Karthikeyan Bhargavan},
    title = {Towards Unified Authorization for Android},
    booktitle = {5th International
    Symposium on Engineering Secure Software and Systems (ESSoS 2013)},
    year = {2013},
    abstract = {Android applications that manage sensitive data such as email and files downloaded from cloud storage services need to protect their data from malware installed on the phone. While prior security analyses have focused on protecting system data such as GPS locations from malware, not much attention has been given to the protection of application data. We show that many popular commercial applications incorrectly use Android authorization mechanisms leading to attacks that steal sensitive data. We argue that formal verification of application behaviors can reveal such errors and we present a formal model in ProVerif that accounts for a variety of Android authorization mechanisms and system services. We write models for four popular applications and analyze them with ProVerif to point out attacks. As a countermeasure, we propose Authzoid, a sample standalone application that lets applications define authorization policies and enforces them on their behalf.},
    publisher = spv,
    series = llncs,
    volume = {7781},
    pages = {42-57}
    }
  • N. Swamy, J. Chen, C. Fournet, P. Strub, K. Bhargavan, and J. Yang, “Secure distributed programming with value-dependent types,” J. funct. program., vol. 23, iss. 4, pp. 402-451, 2013.
    [Bibtex]
    @article{SwamyCFSBY13,
    author = {Nikhil Swamy and
    Juan Chen and
    C{\'e}dric Fournet and
    Pierre-Yves Strub and
    Karthikeyan Bhargavan and
    Jean Yang},
    title = {Secure distributed programming with value-dependent types},
    journal = {J. Funct. Program.},
    volume = {23},
    number = {4},
    year = {2013},
    pages = {402-451},
    ee = {http://dx.doi.org/10.1017/S0956796813000142},
    bibsource = {DBLP, http://dblp.uni-trier.de}
    }

2012

  • [DOI] 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), Pisa, Italy, 2012, pp. 257-272.
    [Bibtex]
    @inproceedings{KS-stm12,
    year = 2012,
    address = {Pisa, Italy},
    author = {K{\"u}nnemann, Robert and Steel, Graham},
    booktitle = {{R}evised {S}elected {P}apers of the 8th {W}orkshop on {S}ecurity and {T}rust {M}anagement ({STM}'12)},
    doi = {10.1007/978-3-642-38004-4_17},
    editor = {J{\o}sang, Audun and Samarati, Pierangela and Petrocchi, Marinella},
    month = sep,
    pages = {257-272},
    publisher = {Springer},
    series = {Lecture Notes in Computer Science},
    title = {{Y}ubi{S}ecure? Formal Security Analysis Results for the {Y}ubikey and {Y}ubi{HSM}},
    url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KS-stm12.pdf},
    volume = {7783},
    abstract = {
    The Yubikey is a small hardware device designed to authenticate a user against network-based services. Despite its widespread adoption (over a million devices have been shipped by Yubico to more than 20 000 customers including Google and Microsoft), the Yubikey protocols have received relatively little security analysis in the academic literature. In the first part of this paper, we give a formal model for the operation of the Yubikey one-time password (OTP) protocol. We prove security properties of the protocol for an unbounded number of fresh OTPs using a protocol analysis tool, tamarin.
    In the second part of the paper, we analyze the security of the protocol with respect to an adversary that has temporary access to the authentication server. To address this scenario, Yubico offers a small Hardware Security Module (HSM) called the YubiHSM, intended to protect keys even in the event of server compromise. We show if the same YubiHSM configuration is used both to set up Yubikeys and run the authentication protocol, then there is inevitably an attack that leaks all of the keys to the attacker. Our discovery of this attack lead to a Yubico security advisory in February 2012. For the case where separate servers are used for the two tasks, we give a configuration for which we can show using the same verification tool that if an adversary that can compromise the server running the Yubikey-protocol, but not the server used to set up new Yubikeys, then he cannot obtain the keys used to produce one-time passwords.
    },
    x-audience = {international},
    x-language = {EN},
    x-town = {Pisa},
    x-country = {IT},
    x-yearstart = {2012}
    }
  • G. Bana, P. Adão, and H. Sakurada, “Computationally Complete Symbolic Attacker in Action,” in Iarcs annual conference on foundations of software technology and theoretical computer science (fsttcs 2012), 2012, p. 546–560.
    [Bibtex]
    @inproceedings{ban:ada:sak:LIPIcs:2012,
    author = {Gergei Bana and Pedro Ad\~ao and Hideki Sakurada},
    title = {{Computationally Complete Symbolic Attacker in Action}},
    booktitle = {IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)},
    series = {Leibniz International Proceedings in Informatics (LIPIcs)},
    year = {2012},
    volume = 18,
    pages = {546--560}
    }
  • G. Bana and H. Comon-Lundh, “Towards unconditional soundness: computationally complete symbolic attacker,” in 2nd conference on principles of security and trust (post 2012), 2012, pp. 189-208.
    [Bibtex]
    @inproceedings{DBLP:conf/post/BanaC12,
    author = {Gergei Bana and
    Hubert Comon-Lundh},
    title = {Towards Unconditional Soundness: Computationally Complete
    Symbolic Attacker},
    booktitle = {2nd Conference on Principles of Security and Trust (POST 2012)},
    year = {2012},
    pages = {189-208},
    abstract = {We consider the question of the adequacy of symbolic models versus computational models for the verification of security protocols. We neither try to include properties in the symbolic model that reflect the properties of the computational primitives nor add computational requirements that enforce the soundness of the symbolic model. We propose in this paper a different approach: everything is possible in the symbolic model, unless it contradicts a computational assumption. In this way, we obtain unconditional soundness almost by construction. And we do not need to assume the absence of dynamic corruption or the absence of key-cycles, which are examples of hypotheses that are always used in related works. We set the basic framework, for arbitrary cryptographic primitives and arbitrary protocols, however for trace security properties only.},
    volume = {7215},
    pages = {189-208},
    series = llncs,
    publisher = spv
    }
  • [DOI] K. Bhargavan, C. Fournet, R. Corin, and E. Zalinescu, “Verified cryptographic implementations for tls,” Acm transactions inf. syst. secur., vol. 15, iss. 1, p. 3:1–3:32, 2012.
    [Bibtex]
    @article{BhargavanFCZ2012,
    author = {Bhargavan, Karthikeyan and Fournet, C{\'e}dric and Corin, Ricardo and Zalinescu, Eugen},
    title = {Verified Cryptographic Implementations for TLS},
    journal = {ACM Transactions Inf. Syst. Secur.},
    issue_date = {March 2012},
    volume = {15},
    number = {1},
    month = Mar,
    year = {2012},
    issn = {1094-9224},
    pages = {3:1--3:32},
    articleno = {3},
    numpages = {32},
    url = {http://doi.acm.org/10.1145/2133375.2133378},
    doi = {10.1145/2133375.2133378},
    acmid = {2133378},
    publisher = {ACM},
    address = {New York, NY, USA}
    }
  • [PDF] D. Cadé and B. Blanchet, “From computationally-proved protocol specifications to implementations,” in 7th international conference on availability, reliability and security (ares 2012), Prague, Czech Republic, 2012, p. 65–74.
    [Bibtex]
    @inproceedings{CadeBlanchetARES12,
    author = {David Cad{\'e} and Bruno Blanchet},
    title = {From Computationally-proved Protocol Specifications to Implementations},
    booktitle = {7th International Conference on Availability, Reliability and Security (AReS 2012)},
    pages = {65--74},
    year = {2012},
    address = {Prague, Czech Republic},
    month = aug,
    publisher = {IEEE},
    x-audience = {international},
    x-language = {EN},
    x-town = {Prague},
    x-country = {CZ},
    url = {https://bblanche.gitlabpages.inria.fr/publications/CadeBlanchetARES12.html},
    pdf = {https://bblanche.gitlabpages.inria.fr/publications/CadeBlanchetARES12.pdf}
    }
  • K. Bhargavan and A. Delignat-Lavaud, “Web-based attacks on host-proof encrypted storage,” in 6th usenix workshop on offensive technologies (woot’12), 2012, p. 97–104.
    [Bibtex]
    @inproceedings{BhargavanDL12,
    author = {Karthikeyan Bhargavan and Antoine Delignat-Lavaud},
    title = {Web-based Attacks on Host-Proof Encrypted Storage},
    booktitle = {6th USENIX Workshop on Offensive Technologies (WOOT'12)},
    year = {2012},
    month = {aug},
    organization = {Usenix},
    pages = {97--104},
    url = {http://prosecco.inria.fr/personal/karthik/pubs/host_proof_woot12.pdf}
    }
  • [PDF] C. Bansal, K. Bhargavan, and S. Maffeis, “Discovering concrete attacks on website authorization by formal analysis,” in 25th ieee computer security foundations symposium (csf’12), Cambridge, MA, USA, 2012, p. 247–262.
    [Bibtex]
    @inproceedings{BansalBM12,
    author = {Chetan Bansal and Karthikeyan Bhargavan and Sergio Maffeis},
    title = {Discovering Concrete Attacks on Website Authorization by Formal Analysis},
    booktitle = {25th IEEE Computer Security Foundations Symposium (CSF'12)},
    optpages = {},
    year = {2012},
    address = {Cambridge, MA, USA},
    month = jun,
    organization = {IEEE},
    pages = {247--262},
    url = {http://prosecco.inria.fr/personal/karthik/pubs/discovering_concrete_attacks_csf12.pdf},
    pdf = {http://prosecco.inria.fr/personal/karthik/pubs/discovering_concrete_attacks_csf12.pdf}
    }
  • [PDF] B. Blanchet, “Automatically verified mechanized proof of one-encryption key exchange,” in 25th ieee computer security foundations symposium (csf’12), Cambridge, MA, USA, 2012, p. 325–339.
    [Bibtex]
    @inproceedings{BlanchetCSF12,
    author = {Bruno Blanchet},
    title = {Automatically Verified Mechanized Proof of One-Encryption Key Exchange},
    booktitle = {25th IEEE Computer Security Foundations Symposium (CSF'12)},
    pages = {325--339},
    year = {2012},
    address = {Cambridge, MA, USA},
    month = jun,
    organization = {IEEE},
    abstract = {
    We present a mechanized proof of the password-based protocol One-Encryption Key Exchange (OEKE) using the computationally-sound protocol prover CryptoVerif. OEKE is a non-trivial protocol, and thus mechanizing its proof provides additional confidence that it is correct.
    This case study was also an opportunity to implement several important extensions of CryptoVerif, useful for proving many other protocols. We have indeed extended CryptoVerif to support the computational Diffie-Hellman assumption. We have also added support for proofs that rely on Shoup's lemma and additional game transformations. In particular, it is now possible to insert case distinctions manually and to merge cases that no longer need to be distinguished. Eventually, some improvements have been added on the computation of the probability bounds for attacks, providing better reductions. In particular, we improve over the standard computation of probabilities when Shoup's lemma is used, which allows us to improve the bound given in a previous manual proof of OEKE, and to show that the adversary can test at most one password per session of the protocol.
    In this paper, we present these extensions, with their application to the proof of OEKE. All steps of the proof, both automatic and manually guided, are verified by CryptoVerif.
    },
    x-audience = {international},
    x-language = {EN},
    x-town = {Cambridge},
    x-country = {US},
    url = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetCSF12.pdf},
    pdf = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetCSF12.pdf}
    }
  • [PDF] M. Paiola and B. Blanchet, “Verification of security protocols with lists: from length one to unbounded length,” in First conference on principles of security and trust (post’12), Tallinn, Estonia, 2012, p. 69–88.
    [Bibtex]
    @inproceedings{PaiolaBlanchetPOST12,
    author = {Miriam Paiola and Bruno Blanchet},
    title = {Verification of Security Protocols with Lists:
    from Length One to Unbounded Length},
    booktitle = {First Conference on Principles of Security and Trust (POST'12)},
    pages = {69--88},
    year = 2012,
    editor = {Pierpaolo Degano and Joshua Guttman},
    volume = 7215,
    series = lncs,
    address = {Tallinn, Estonia},
    month = mar,
    publisher = spv,
    abstract = {We present a novel, simple technique for proving secrecy properties for
    security protocols that manipulate lists of unbounded length, for
    an unbounded number of sessions.
    More specifically, our technique relies on the Horn clause
    approach used in the automatic verifier ProVerif: we show that if
    a protocol is proven secure by our technique with lists of length
    one, then it is secure for lists of unbounded length.
    Interestingly, this theorem relies on approximations made by our
    verification technique: in general, secrecy for lists of length
    one does not imply secrecy for lists of unbounded length.
    Our result can be used in particular to prove secrecy properties
    for group protocols with an unbounded number of participants and
    for some XML protocols (web services) with ProVerif.},
    x-audience = {international},
    x-language = {EN},
    x-town = {Tallinn},
    x-country = {EE},
    x-yearstart = {2012},
    url = {http://prosecco.gforge.inria.fr/personal/mpaiola/publications/articles/PaiolaBlanchetPOST12LV.pdf},
    pdf = {http://prosecco.gforge.inria.fr/personal/mpaiola/publications/articles/PaiolaBlanchetPOST12LV.pdf}
    }
  • [PDF] B. Blanchet, “Security protocol verification: symbolic and computational models,” in First conference on principles of security and trust (post’12), Tallinn, Estonia, 2012, p. 3–29.
    [Bibtex]
    @inproceedings{BlanchetETAPS12,
    author = {Bruno Blanchet},
    title = {Security Protocol Verification: Symbolic and Computational Models},
    booktitle = {First Conference on Principles of Security and Trust (POST'12)},
    pages = {3--29},
    year = 2012,
    editor = {Pierpaolo Degano and Joshua Guttman},
    volume = 7215,
    series = lncs,
    address = {Tallinn, Estonia},
    month = mar,
    publisher = spv,
    abstract = {Security protocol verification has been a very active
    research area
    since the 1990s. This paper surveys various approaches in this
    area, considering the verification in the symbolic model, as
    well as the more recent approaches that rely on the computational
    model or that verify protocol implementations rather than
    specifications. Additionally, we briefly describe our symbolic
    security protocol verifier ProVerif and situate it among these approaches.},
    x-audience = {international},
    x-language = {EN},
    x-town = {Tallinn},
    x-country = {EE},
    url = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetETAPS12.pdf},
    pdf = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetETAPS12.pdf}
    }
  • [PDF] B. Blanchet, “Mechanizing game-based proofs of security protocols,” in Software safety and security – tools for analysis and verification, T. Nipkow, O. Grumberg, and B. Hauptmann, Eds., Ios press, 2012, vol. 33, p. 1–25.
    [Bibtex]
    @incollection{BlanchetMOD11,
    author = {Bruno Blanchet},
    title = {Mechanizing Game-Based Proofs of Security Protocols},
    booktitle = {Software Safety and Security - Tools for Analysis and Verification},
    pages = {1--25},
    publisher = {IOS Press},
    year = 2012,
    editor = {Tobias Nipkow and Olga Grumberg and Benedikt Hauptmann},
    volume = 33,
    series = {NATO Science for Peace and Security Series -- D: Information and Communication Security},
    month = may,
    ibsn = {978-1-61499-027-7},
    note = {Proceedings of the summer school MOD 2011},
    abstract = {After a short introduction to the field of security
    protocol verification, we present the automatic
    protocol verifier CryptoVerif. In contrast to most
    previous protocol verifiers, CryptoVerif does not
    rely on the Dolev-Yao model, but on the
    computational model. It produces proofs presented as
    sequences of games, like those manually done by
    cryptographers; these games are formalized in a
    probabilistic process calculus. CryptoVerif provides
    a generic method for specifying security properties
    of the cryptographic primitives. It can prove
    secrecy and correspondence properties (including
    authentication). It produces proofs valid for any
    number of sessions, in the presence of an active
    adversary. It also provides an explicit formula for
    the probability of success of an attack against the
    protocol, as a function of the probability of
    breaking each primitive and of the number of
    sessions.},
    x-audience = {international},
    x-language = {EN},
    url = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetMOD11.pdf},
    pdf = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetMOD11.pdf}
    }
  • K. Bhargavan, “Towards the automated verification of cryptographic protocol implementations,” Mémoire d’habilitation PhD Thesis, 2012.
    [Bibtex]
    @phdthesis{BhargavanHDR,
    author = {Karthikeyan Bhargavan},
    title = {Towards the Automated Verification of Cryptographic Protocol Implementations},
    school = {\'{E}cole Normale Sup\'{e}rieure},
    year = 2012,
    type = {M{\'e}moire d'habilitation},
    month = may
    }
  • A. Pironti, P. Strub, and K. Bhargavan, “Identifying Website Users by TLS Traffic Analysis: New Attacks and Effective Countermeasures,” INRIA, Research Report RR-8067, 2012.
    [Bibtex]
    @techreport{pironti:hal-00732449,
    author = {Pironti, Alfredo and Strub, Pierre-Yves and Bhargavan, Karthikeyan},
    title = {{Identifying Website Users by TLS Traffic Analysis: New Attacks and Effective Countermeasures}},
    type = {Research Report},
    year = {2012},
    month = Sep,
    institution = {INRIA},
    number = {RR-8067},
    x-id-hal = {hal-00732449},
    note = {INRIA Technical Report RR-8067}
    }
  • P. Bettassa Copet, A. Pironti, D. Pozza, R. Sisto, and P. Vivoli, “Visual model-driven design, verification and implementation of security protocols,” in Ieee international symposium on high assurance systems engineering (hase 12), 2012.
    [Bibtex]
    @inproceedings{BettassaPPSV12,
    title = {Visual Model-Driven Design, Verification and Implementation of Security Protocols},
    booktitle = {IEEE International Symposium on High Assurance Systems Engineering (HASE 12)},
    year = {2012},
    note = {Short paper},
    publisher = {IEEE Computer Security},
    organization = {IEEE Computer Security},
    author = {Bettassa Copet, Piergiuseppe and Alfredo Pironti and Davide Pozza and Riccardo Sisto and Pietro Vivoli},
    x-proceedings = {yes},
    x-international-audience = {yes}
    }
  • A. Pironti, D. Pozza, and R. Sisto, “Formally-based semi-automatic implementation of an open security protocol,” Journal of systems and software, vol. 85, p. 835{–}849, 2012.
    [Bibtex]
    @article{PirontiPS11,
    title = {Formally-Based Semi-Automatic Implementation of an Open Security Protocol},
    journal = {Journal of Systems and Software},
    volume = {85},
    year = {2012},
    pages = {835{\textendash}849},
    publisher = {Elsevier},
    author = {Alfredo Pironti and Davide Pozza and Riccardo Sisto},
    x-editorial-board = {yes},
    x-international-audience = {yes}
    }
  • M. Avalle, A. Pironti, and R. Sisto, “Formal verification of security protocol implementations: a survey,” Formal aspects of computing, pp. 1-25, 2012.
    [Bibtex]
    @article{41,
    title = {Formal verification of security protocol implementations: a survey},
    journal = {Formal Aspects of Computing},
    year = {2012},
    pages = {1-25},
    author = {Matteo Avalle and Alfredo Pironti and Riccardo Sisto},
    x-editorial-board = {yes},
    x-international-audience = {yes}
    }
  • A. Pironti and R. Sisto, “Safe abstractions of data encodings in formal security protocol models,” Formal aspects of computing, pp. 1-43, 2012.
    [Bibtex]
    @article{PirontiS12,
    title = {Safe Abstractions of Data Encodings in Formal Security Protocol Models},
    journal = {Formal Aspects of Computing},
    year = {2012},
    pages = {1-43},
    author = {Alfredo Pironti and Riccardo Sisto},
    x-editorial-board = {yes},
    x-international-audience = {yes}
    }
  • R. Bardou, R. Focardi, Y. Kawamoto, L. Simionato, G. Steel, and J. Tsay, “Efficient Padding Oracle Attacks on Cryptographic Hardware,” INRIA, Research Report RR-7944, 2012.
    [Bibtex]
    @techreport{bardou:hal-00691958,
    author = {Bardou, Romain and Focardi, Riccardo and Kawamoto, Yusuke and Simionato, Lorenzo and Steel, Graham and Tsay, Joe-Kai},
    title = {{Efficient Padding Oracle Attacks on Cryptographic Hardware}},
    type = {Research Report},
    pages = {19},
    year = {2012},
    month = Apr,
    institution = {INRIA},
    number = {RR-7944},
    x-id-hal = {hal-00691958},
    note = {INRIA Technical Report RR-7944}
    }
  • V. Cortier, G. Steel, and C. Wiedling, “Revoke and Let Live: A Secure Key Revocation API for Cryptographic Devices,” INRIA, Research Report RR-7949, 2012.
    [Bibtex]
    @techreport{cortier:hal-00721945,
    author = {Cortier, V{\'e}ronique and Steel, Graham and Wiedling, Cyrille},
    title = {{Revoke and Let Live: A Secure Key Revocation API for Cryptographic Devices}},
    type = {Research Report},
    pages = {41},
    year = {2012},
    month = Jul,
    institution = {INRIA},
    number = {RR-7949},
    x-id-hal = {hal-00721945},
    note = {INRIA Technical Report RR-7949}
    }
  • R. Bardou, R. Focardi, Y. Kawamoto, L. Simionato, G. Steel, and J. Tsay, “Efficient padding oracle attacks on cryptographic hardware,” in Crypto, 2012, p. 608–625.
    [Bibtex]
    @inproceedings{BardouFKSST12,
    author = {Romain Bardou and
    Riccardo Focardi and
    Yusuke Kawamoto and
    Lorenzo Simionato and
    Graham Steel and
    Joe-Kai Tsay},
    title = {Efficient Padding Oracle Attacks on Cryptographic Hardware},
    booktitle = {CRYPTO},
    year = {2012},
    pages = {608--625}
    }

2011

  • [PDF] G. Steel, “Formal analysis of security APIs,” Mémoire d’habilitation PhD Thesis, 2011.
    [Bibtex]
    @phdthesis{steel-HDR11,
    author = {Steel, Graham},
    month = mar,
    school = {{\'E}cole Normale Sup{\'e}rieure de Cachan, France},
    type = {M{\'e}moire d'habilitation},
    title = {Formal Analysis of Security {API}s},
    year = {2011},
    nmonth = {3},
    url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/hdr-GS.pdf},
    pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/hdr-GS.pdf},
    lsv-category = {thes},
    wwwpublic = {public and ccsb}
    }
  • [PDF] J. Bengtson, K. Bhargavan, C. Fournet, A. D. Gordon, and S. Maffeis, “Refinement types for secure implementations,” Acm trans. program. lang. syst., vol. 33, iss. 2, p. 8, 2011.
    [Bibtex]
    @article{BengtsonBFGM11,
    author = {Jesper Bengtson and
    Karthikeyan Bhargavan and
    C{\'e}dric Fournet and
    Andrew D. Gordon and
    Sergio Maffeis},
    title = {Refinement types for secure implementations},
    journal = {ACM Trans. Program. Lang. Syst.},
    volume = {33},
    number = {2},
    year = {2011},
    pages = {8},
    pdf = {http://prosecco.inria.fr/personal/karthik/pubs/refinement-types-for-secure-implementations-toplas11.pdf},
    url = {http://prosecco.inria.fr/personal/karthik/pubs/refinement-types-for-secure-implementations-toplas11.pdf},
    ee = {http://doi.acm.org/10.1145/1890028.1890031},
    bibsource = {DBLP, http://dblp.uni-trier.de}
    }
  • [PDF] N. Swamy, J. Chen, C. Fournet, P. Strub, K. Bhargavan, and J. Yang, “Secure distributed programming with value-dependent types,” in 16th acm sigplan international conference on functional programming, 2011, pp. 266-278.
    [Bibtex]
    @inproceedings{SwamyCFSBY11,
    author = {Nikhil Swamy and
    Juan Chen and
    C{\'e}dric Fournet and
    Pierre-Yves Strub and
    Karthikeyan Bhargavan and
    Jean Yang},
    title = {Secure distributed programming with value-dependent types},
    booktitle = {16th ACM SIGPLAN international conference
    on Functional Programming},
    year = {2011},
    pages = {266-278},
    pdf = {http://research.microsoft.com/pubs/150012/icfp-camera-ready.pdf},
    url = {http://research.microsoft.com/apps/pubs/default.aspx?id=150012},
    ee = {http://doi.acm.org/10.1145/2034773.2034811},
    bibsource = {DBLP, http://dblp.uni-trier.de}
    }
  • C. Fournet, K. Bhargavan, and A. D. Gordon, “Cryptographic verification by typing for a sample protocol implementation,” in Foundations of security analysis and design vi (fosad’10), 2011, pp. 66-100.
    [Bibtex]
    @inproceedings{FournetBG10,
    author = {C{\'e}dric Fournet and
    Karthikeyan Bhargavan and
    Andrew D. Gordon},
    title = {Cryptographic Verification by Typing for a Sample Protocol
    Implementation},
    booktitle = {Foundations of Security Analysis and Design VI (FOSAD'10)},
    year = {2011},
    pages = {66-100},
    ee = {http://dx.doi.org/10.1007/978-3-642-23082-0_3},
    bibsource = {DBLP, http://dblp.uni-trier.de}
    }
  • [PDF] B. Blanchet, “Using Horn clauses for analyzing security protocols,” in Formal models and techniques for analyzing security protocols, V. Cortier and S. Kremer, Eds., Ios press, 2011, vol. 5, p. 86–111.
    [Bibtex]
    @incollection{BlanchetBook09,
    author = {Bruno Blanchet},
    title = {Using {H}orn Clauses for Analyzing Security Protocols},
    booktitle = {Formal Models and Techniques for Analyzing Security Protocols},
    publisher = {IOS Press},
    pages = {86--111},
    volume = 5,
    series = {Cryptology and Information Security Series},
    month = mar,
    year = 2011,
    editor = {V{\'e}ronique Cortier and Steve Kremer},
    isbn = {978-1-60750-713-0},
    url = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetBook09.pdf},
    pdf = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetBook09.pdf}
    }
  • S. Kremer, G. Steel, and B. Warinschi, “Security for key management interfaces,” in Proceedings of the 24th IEEE Computer Security Foundations Symposium (CSF’11), Cernay-la-Ville, France, 2011, pp. 266-280.
    [Bibtex]
    @inproceedings{KSW-csf11,
    abstract = {We propose a much-needed formal definition of
    security for cryptographic key management APIs. The
    advantages of our definition are that it is general,
    intuitive, and applicable to security proofs in both
    symbolic and computational models of cryptography.
    Our definition relies on an idealized API which
    allows only the most essential functions for
    generating, exporting and importing keys, and takes
    into account dynamic corruption of keys. Based on
    this we can define the security of more expressive
    APIs which support richer functionality. We
    illustrate our approach by showing the security of
    APIs both in symbolic and computational models.},
    address = {Cernay-la-Ville, France},
    author = {Kremer, Steve and Steel, Graham and
    Warinschi, Bogdan},
    booktitle = {{P}roceedings of the 24th {IEEE} {C}omputer
    {S}ecurity {F}oundations {S}ymposium ({CSF}'11)},
    month = jun,
    pages = {266-280},
    publisher = {{IEEE} Computer Society Press},
    title = {Security for Key Management Interfaces},
    year = {2011},
    acronym = {{CSF}'11},
    nmonth = {6},
    longpdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2011-07.pdf},
    longps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2011-07.ps},
    lsv-category = {intc},
    lsv-status = {apar},
    wwwpublic = {public}
    }
  • [PDF] 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), Cernay-la-Ville, France, 2011, pp. 66-82.
    [Bibtex]
    @inproceedings{DKRS-csf11,
    abstract = {We~present a Horn-clause-based framework for
    analysing security protocols that use platform
    configuration registers~(PCRs), which are registers
    for maintaining state inside the Trusted Platform
    Module~(TPM). In~our model, the~PCR state space is
    unbounded, and our experience shows that a na\EFve
    analysis using ProVerif or SPASS does not terminate.
    To address this, we extract a set of instances of the
    Horn clauses of our model, for which ProVerif does
    terminate on our examples. We~prove the soundness of
    this extraction process: no~attacks are lost,
    that~is, any query derivable in the more general set
    of clauses is also derivable from the extracted
    instances. The~effectiveness of our framework is
    demonstrated in two case studies: a~simplified
    version of Microsoft Bitlocker, and a digital
    envelope protocol that allows a user to choose
    whether to perform a decryption, or to verifiably
    renounce the ability to perform the decryption.},
    address = {Cernay-la-Ville, France},
    author = {Delaune, St{\'e}phanie and Kremer, Steve and
    Ryan, Mark D. and Steel, Graham},
    booktitle = {{P}roceedings of the 24th {IEEE} {C}omputer
    {S}ecurity {F}oundations {S}ymposium ({CSF}'11)},
    month = jun,
    pages = {66-82},
    publisher = {{IEEE} Computer Society Press},
    title = {Formal analysis of protocols based on {TPM} state
    registers},
    year = {2011},
    acronym = {{CSF}'11},
    nmonth = {6},
    url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKRS-csf11.pdf},
    pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKRS-csf11.pdf},
    lsv-category = {intc},
    lsv-status = {apar},
    wwwpublic = {public}
    }
  • [PDF] M. Dahl, S. Delaune, and G. Steel, “Formal analysis of privacy for anonymous location based services,” in Proceedings of the Workshop on Theory of Security and Applications (TOSCA’11), Saarbrücken, Germany, 2011.
    [Bibtex]
    @inproceedings{DDS-tosca11,
    abstract = {We propose a framework for formal analysis of privacy
    in location based services such as anonymous
    electronic toll collection. We give a formal
    definition of privacy, and apply it to the VPriv
    scheme for vehicular services. We analyse the
    resulting model using the ProVerif tool, concluding
    that our privacy property holds only if certain
    conditions are met by the implementation. Our
    analysis includes some novel features such as the
    formal modelling of privacy for a protocol that
    relies on interactive zero-knowledge proofs of
    knowledge and list permutations.},
    address = {Saarbr{\"u}cken, Germany},
    author = {Dahl, Morten and Delaune, St{\'e}phanie and
    Steel, Graham},
    booktitle = {{P}roceedings of the {W}orkshop on {T}heory of
    {S}ecurity and {A}pplications ({TOSCA}'11)},
    month = mar # {-} # apr,
    title = {Formal Analysis of Privacy for Anonymous Location
    Based Services},
    year = {2011},
    acronym = {{TOSCA}'11},
    nmonth = {3},
    url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DDS-tosca11.pdf},
    pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DDS-tosca11.pdf},
    lsv-category = {intc},
    lsv-status = {apar},
    wwwpublic = {public}
    }
  • [PDF] B. Blanchet, “A second look at Shoup’s lemma,” in Workshop on formal and computational cryptography (fcc 2011), Paris, France, 2011.
    [Bibtex]
    @inproceedings{BlanchetFCC11,
    author = {Bruno Blanchet},
    title = {A second look at {S}houp's lemma},
    booktitle = {Workshop on Formal and Computational Cryptography (FCC 2011)},
    year = 2011,
    address = {Paris, France},
    month = jun,
    url = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetFCC11.pdf},
    pdf = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetFCC11.pdf}
    }

2010

  • [PDF] [DOI] S. Delaune, S. Kremer, and G. Steel, “Formal analysis of PKCS\#11 and proprietary extensions,” Journal of computer security, vol. 18, iss. 6, pp. 1211-1245, 2010.
    [Bibtex]
    @article{DKS-jcs09,
    abstract = {PKCS\#11 denes an API for cryptographic devices that
    has been widely adopted in industry. However, it has
    been shown to be vulnerable to a variety of attacks
    that could, for example, compromise the sensitive
    keys stored on the device. In this paper, we set out
    a formal model of the operation of the API, which
    diers from previous security API models notably in
    that it accounts for non-monotonic mutable global
    state. We give decidability results for our
    formalism, and describe an implementation of the
    resulting decision procedure using the model checker
    NuSMV. We report some new attacks and prove the
    safety of some congurations of the API in our model.
    We also analyse proprietary extensions proposed by
    nCipher (Thales) and Eracom (Safenet), designed to
    address the shortcomings of PKCS\#11.},
    author = {Delaune, St{\'e}phanie and Kremer, Steve and
    Steel, Graham},
    doi = {10.3233/JCS-2009-0394},
    journal = {Journal of Computer Security},
    month = nov,
    number = {6},
    pages = {1211-1245},
    publisher = {{IOS} Press},
    title = {Formal Analysis of {PKCS\#11} and Proprietary
    Extensions},
    volume = {18},
    year = {2010},
    nmonth = {11},
    url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKS-jcs09.pdf},
    pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKS-jcs09.pdf},
    lsv-category = {jour},
    wwwpublic = {public and ccsb}
    }
  • [PDF] [DOI] 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), Pisa, Italy, 2010, pp. 111-125.
    [Bibtex]
    @inproceedings{DKRS-fast10,
    abstract = {The Trusted Platform Module~(TPM) is a hardware chip
    designed to enable computers to achieve a greater
    level of security than is possible in software alone.
    To this end, the TPM provides a way to store
    cryptographic keys and other sensitive data in its
    shielded memory. Through its API, one can use those
    keys to achieve some security goals. The TPM is a
    complex security component, whose specification
    consists of more than \(700\)~pages.\par We model a
    collection of four TPM commands, and we identify and
    formalise their security properties. Using the tool
    ProVerif, we rediscover some known attacks and some
    new variations on them. We propose modifications to
    the API and verify our properties for the modified
    API.},
    address = {Pisa, Italy},
    author = {Delaune, St{\'e}phanie and Kremer, Steve and
    Ryan, Mark D. and Steel, Graham},
    booktitle = {{R}evised {S}elected {P}apers of the 7th
    {I}nternational {W}orkshop on {F}ormal {A}spects in
    {S}ecurity and {T}rust ({FAST}'10)},
    doi = {10.1007/978-3-642-19751-2_8},
    editor = {Degano, Pierpaolo and Etalle, Sandro and
    Guttman, Joshua},
    month = sep,
    pages = {111-125},
    publisher = {Springer},
    series = {Lecture Notes in Computer Science},
    title = {A~Formal Analysis of Authentication in the {TPM}},
    volume = {6561},
    year = {2010},
    acronym = {{FAST}'10},
    nmonth = {9},
    url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKRS-fast10.pdf},
    pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKRS-fast10.pdf},
    ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DKRS-fast10.ps},
    lsv-category = {intc},
    wwwpublic = {public and ccsb}
    }
  • [PDF] [DOI] 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), Chicago, Illinois, USA, 2010, pp. 260-269.
    [Bibtex]
    @inproceedings{BCFS-ccs10,
    abstract = {We show how to extract sensitive cryptographic keys
    from a variety of commercially available tamper
    resistant cryptographic security tokens, exploiting
    vulnerabilities in their RSA PKCS\#11 based APIs. The
    attacks are performed by Tookan, an automated tool we
    have developed, which reverse-engineers the
    particular token in use to deduce its functionality,
    constructs a model of its API for a model checker,
    and then executes any attack trace found by the model
    checker directly on the token. We describe the
    operation of Tookan and give results of testing the
    tool on 17 commercially available tokens: 9~were
    vulnerable to attack, while the other 8 had severely
    restricted functionality. One of the attacks found by
    the model checker has not previously appeared in the
    literature. We show how Tookan may be used to verify
    patches to insecure devices, and give a secure
    configuration that we have implemented in a patch to
    a software token simulator. This is the first such
    configuration to appear in the literature that does
    not require any new cryptographic mechanisms to be
    added to the standard. We comment on lessons for
    future key management APIs.},
    address = {Chicago, Illinois, USA},
    author = {Bortolozzo, Matteo and Centenaro, Matteo and
    Focardi, Riccardo and Steel, Graham},
    booktitle = {{P}roceedings of the 17th {ACM} {C}onference on
    {C}omputer and {C}ommunications {S}ecurity
    ({CCS}'10)},
    doi = {10.1145/1866307.1866337},
    month = oct,
    pages = {260-269},
    publisher = {ACM Press},
    title = {Attacking and Fixing {PKCS}\#11 Security Tokens},
    year = {2010},
    acronym = {{CCS}'10},
    nmonth = {10},
    url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCFS-ccs10.pdf},
    pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCFS-ccs10.pdf},
    lsv-category = {intc},
    wwwpublic = {public and ccsb}
    }
  • [PDF] [DOI] 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), Athens, Greece, 2010, pp. 55-70.
    [Bibtex]
    @inproceedings{DDS-esorics10,
    abstract = {Safety critical applications for recently proposed
    vehicle to vehicle ad-hoc networks~(VANETs) rely on a
    beacon signal, which poses a threat to privacy since
    it could allow a vehicle to be tracked. Mix-zones,
    where vehicles encrypt their transmissions and then
    change their identifiers, have been proposed as a
    solution to this problem. \par In this work,
    we~describe a formal analysis of mix-zones. We~model
    a mix-zone and propose a formal definition of privacy
    for such a zone. We~give a set of necessary
    conditions for any mix-zone protocol to preserve
    privacy. We~analyse, using the tool ProVerif,
    a~particular proposal for key distribution in
    mix-zones, the CMIX protocol. We~report attacks on
    privacy and we propose a fix.},
    address = {Athens, Greece},
    author = {Dahl, Morten and Delaune, St{\'e}phanie and
    Steel, Graham},
    booktitle = {{P}roceedings of the 15th {E}uropean {S}ymposium on
    {R}esearch in {C}omputer {S}ecurity ({ESORICS}'10)},
    doi = {10.1007/978-3-642-15497-3_4},
    editor = {Gritzalis, Dimitris and Preneel, Bart},
    month = sep,
    pages = {55-70},
    publisher = {Springer},
    series = {Lecture Notes in Computer Science},
    title = {Formal Analysis of Privacy for Vehicular Mix-Zones},
    volume = {6345},
    year = {2010},
    acronym = {{ESORICS}'10},
    nmonth = {9},
    url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DDS-esorics10.pdf},
    pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DDS-esorics10.pdf},
    ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DDS-esorics10.ps},
    lsv-category = {intc},
    wwwpublic = {public and ccsb}
    }
  • K. Bhargavan, C. Fournet, and A. D. Gordon, “Modular verification of security protocol code by typing,” in 37th acm sigplan-sigact symposium on principles of programming languages (popl’10), 2010, pp. 445-456.
    [Bibtex]
    @inproceedings{BhargavanFG10,
    author = {Karthikeyan Bhargavan and
    C{\'e}dric Fournet and
    Andrew D. Gordon},
    title = {Modular verification of security protocol code by typing},
    booktitle = {37th ACM SIGPLAN-SIGACT Symposium on
    Principles of Programming Languages (POPL'10)},
    year = {2010},
    pages = {445-456},
    ee = {http://doi.acm.org/10.1145/1706299.1706350},
    bibsource = {DBLP, http://dblp.uni-trier.de}
    }
  • K. Bhargavan, C. Fournet, and N. Guts, “Typechecking higher-order security libraries,” in 8th asian symposium on programming languages and systems, 2010, pp. 47-62.
    [Bibtex]
    @inproceedings{BhargavanFG10aplas,
    author = {Karthikeyan Bhargavan and
    C{\'e}dric Fournet and
    Nataliya Guts},
    title = {Typechecking Higher-Order Security Libraries},
    booktitle = {8th Asian Symposium on Programming Languages and Systems},
    year = {2010},
    pages = {47-62},
    ee = {http://dx.doi.org/10.1007/978-3-642-17164-2_5},
    bibsource = {DBLP, http://dblp.uni-trier.de}
    }
  • [PDF] B. Blanchet and D. Pointcheval, “The computational and decisional Diffie-Hellman assumptions in CryptoVerif,” in Workshop on formal and computational cryptography (fcc 2010), Edimburgh, United Kingdom, 2010.
    [Bibtex]
    @inproceedings{BlanchetPointchevalFCC10,
    author = {Bruno Blanchet and David Pointcheval},
    title = {The computational and decisional {D}iffie-{H}ellman assumptions in {C}rypto{V}erif},
    booktitle = {Workshop on Formal and Computational Cryptography (FCC 2010)},
    year = 2010,
    address = {Edimburgh, United Kingdom},
    month = jul,
    url = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetPointchevalFCC10.pdf},
    pdf = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetPointchevalFCC10.pdf}
    }

2009

  • [PDF] B. Blanchet, “Automatic verification of correspondences for security protocols,” Journal of computer security, vol. 17, iss. 4, p. 363–434, 2009.
    [Bibtex]
    @article{BlanchetJCS08,
    author = {Bruno Blanchet},
    title = {Automatic Verification of Correspondences for Security Protocols},
    journal = {Journal of Computer Security},
    year = 2009,
    volume = 17,
    number = 4,
    pages = {363--434},
    month = jul,
    url = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetJCS08.pdf},
    pdf = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetJCS08.pdf}
    }
  • [PDF] M. ‘i, B. Blanchet, and H. Comon-Lundh, “Models and proofs of protocol security: a progress report,” in 21st international conference on computer aided verification (cav’09), Grenoble, France, 2009, p. 35–49.
    [Bibtex]
    @inproceedings{AbadiBlanchetComonCAV09,
    author = {Mart{\'\i}n Abadi and Bruno Blanchet and Hubert Comon-Lundh},
    title = {Models and Proofs of Protocol Security: A Progress Report},
    booktitle = {21st International Conference on Computer Aided Verification (CAV'09)},
    pages = {35--49},
    year = 2009,
    editor = {Ahmed Bouajjani and Oded Maler},
    volume = 5643,
    series = lncs,
    address = {Grenoble, France},
    month = jun,
    publisher = spv,
    url = {https://bblanche.gitlabpages.inria.fr/publications/AbadiBlanchetComonCAV09.pdf},
    pdf = {https://bblanche.gitlabpages.inria.fr/publications/AbadiBlanchetComonCAV09.pdf}
    }
  • [PDF] [DOI] 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), Oslo, Norway, 2009, pp. 88-103.
    [Bibtex]
    @inproceedings{FLS-nordsec09,
    abstract = {We~propose a countermeasure for a class of known
    attacks on the PIN processing API used in the ATM
    (cash machine) network. This API controls access to
    the tamper-resistant Hardware Security Modules where
    PIN encryption, decryption and verification takes
    place. The~attacks are differential attacks, whereby
    an attacker gains information about the plaintext
    values of encrypted customer PINs by making changes
    to the non-confidential inputs to a command.
    Our~proposed fix adds an integrity check to the
    parameters passed to the command. It~is novel in that
    it involves very little change to the existing ATM
    network infrastructure.},
    address = {Oslo, Norway},
    author = {Focardi, Riccardo and Luccio, Flaminia L. and
    Steel, Graham},
    booktitle = {{P}roceedings of the 14th {N}ordic {W}orkshop on
    {S}ecure {IT} {S}ystems ({NordSec}'09)},
    doi = {10.1007/978-3-642-04766-4_7},
    editor = {J{\o}sang, Audun and Maseng, Torleiv and
    Knapskog, Svein Johan},
    month = oct,
    pages = {88-103},
    publisher = {Springer},
    series = {Lecture Notes in Computer Science},
    title = {Blunting Differential Attacks on {PIN} Processing
    {API}s},
    volume = {5838},
    year = {2009},
    acronym = {{NordSec}'09},
    nmonth = {10},
    url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FLS-nordsec09.pdf},
    pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FLS-nordsec09.pdf},
    lsv-category = {intc},
    wwwpublic = {public and ccsb}
    }
  • [PDF] [DOI] 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), Saint~Malo, France, 2009, pp. 53-68.
    [Bibtex]
    @inproceedings{CFLS-esorics09,
    abstract = {We examine some known attacks on the PIN verification
    framework, based on weaknesses of the security API
    for the tamper-resistant Hardware Security Modules
    used in the network. We specify this API in an
    imperative language with cryptographic primitives,
    and show how its flaws are captured by a notion of
    robustness that extends the one of Myers, Sabelfeld
    and Zdancewic to our cryptographic setting.
    We~propose an improved API, give an extended type
    system for assuring integrity and for preserving
    confidentiality via randomized and non-randomized
    encryptions, and show our new API to be
    type-checkable.},
    address = {Saint~Malo, France},
    author = {Centenaro, Matteo and Focardi, Riccardo and
    Luccio, Flaminia L. and Steel, Graham},
    booktitle = {{P}roceedings of the 14th {E}uropean {S}ymposium on
    {R}esearch in {C}omputer {S}ecurity ({ESORICS}'09)},
    doi = {10.1007/978-3-642-04444-1_4},
    editor = {Backes, Michael and Ning, Peng},
    month = sep,
    pages = {53-68},
    publisher = {Springer},
    series = {Lecture Notes in Computer Science},
    title = {Type-based Analysis of {PIN} Processing {API}s},
    volume = {5789},
    year = {2009},
    acronym = {{ESORICS}'09},
    nmonth = {9},
    url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CFLS-esorics09.pdf},
    pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CFLS-esorics09.pdf},
    lsv-category = {intc},
    wwwpublic = {public and ccsb}
    }
  • [PDF] [DOI] 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), Saint~Malo, France, 2009, pp. 605-620.
    [Bibtex]
    @inproceedings{CS-esorics09,
    abstract = {Security APIs are used to define the boundary between
    trusted and untrusted code. The security properties
    of existing APIs are not always clear. In~this paper,
    we~give a new generic API for managing symmetric keys
    on a trusted cryptographic device. We state and prove
    security properties for our API. In~particular, our
    API offers a high level of security even when the
    host machine is controlled by an attacker. Our API is
    generic in the sense that it can implement a wide
    variety of (symmetric~key) protocols. As a proof of
    concept, we give an algorithm for automatically
    instantiating the API commands for a given key
    management protocol. We demonstrate the algorithm on
    a set of key establishment protocols from the
    Clark-Jacob suite.},
    address = {Saint~Malo, France},
    author = {Cortier, V{\'e}ronique and Steel, Graham},
    booktitle = {{P}roceedings of the 14th {E}uropean {S}ymposium on
    {R}esearch in {C}omputer {S}ecurity ({ESORICS}'09)},
    doi = {10.1007/978-3-642-04444-1_37},
    editor = {Backes, Michael and Ning, Peng},
    month = sep,
    pages = {605-620},
    publisher = {Springer},
    series = {Lecture Notes in Computer Science},
    title = {A~generic security {API} for symmetric key management
    on cryptographic devices},
    volume = {5789},
    year = {2009},
    acronym = {{ESORICS}'09},
    nmonth = {9},
    url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CS-esorics09.pdf},
    pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CS-esorics09.pdf},
    lsv-category = {intc},
    wwwpublic = {public and ccsb}
    }
  • [PDF] [DOI] 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), York, UK, 2009, pp. 173-192.
    [Bibtex]
    @inproceedings{KAS-arspawits09,
    abstract = {Security API analysis typically only considers a
    subset of an API's functions, with results bounded by
    the number of function calls. Furthermore, attacks
    involving partial leakage of sensitive information
    are usually not covered. Type-based static analysis
    has the potential to alleviate these shortcomings. To
    that end, we present a type system for secure
    information flow based upon the one of Volpano, Smith
    and Irvine, extended with types for cryptographic
    keys and ciphertext similar to those in Sumii and
    Pierce. In~contrast to some other type systems, the
    encryption and decryption of keys does not require
    special treatment. We show that a well-typed sequence
    of commands is non-interferent, based upon a
    definition of indistinguishability where, in certain
    circumstances, the adversary can distinguish between
    ciphertexts that correspond to encrypted public
    data.},
    address = {York, UK},
    author = {Keighren, Gavin and Aspinall, David and
    Steel, Graham},
    booktitle = {{R}evised {S}elected {P}apers of the {J}oint
    {W}orkshop on {A}utomated {R}easoning for {S}ecurity
    {P}rotocol {A}nalysis and {I}ssues in the {T}heory of
    {S}ecurity ({ARSPA-WITS}'09)},
    doi = {10.1007/978-3-642-03459-6_12},
    editor = {Degano, Pierpaolo and Vigan{\`o}, Luca},
    month = aug,
    pages = {173-192},
    publisher = {Springer},
    series = {Lecture Notes in Computer Science},
    title = {Towards a Type System for Security {API}s},
    volume = {5511},
    year = {2009},
    acronym = {{ARSPA-WITS}'09},
    nmonth = {8},
    conf-year = {2009},
    conf-month = mar,
    url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KAS-arspawits09.pdf},
    pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KAS-arspawits09.pdf},
    lsv-category = {intc},
    wwwpublic = {public and ccsb}
    }
  • [PDF] [DOI] 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), York, UK, 2009, pp. 92-106.
    [Bibtex]
    @inproceedings{FS-arspawits09,
    abstract = {We extend Delaune, Kremer and Steel's framework for
    analysis of PKCS#11-based APIs from bounded to
    unbounded fresh data. We achieve this by: formally
    defining the notion of an \emph{attribute policy};
    showing that a well-designed API should have a
    certain class of policy we call \emph{complete};
    showing that APIs with complete policies may be
    safely abstracted to APIs where the attributes are
    fixed; and proving that these \emph{static} APIs can
    be analysed in a small bounded model such that
    security properties will hold for the unbounded case.
    We automate analysis in our framework using the
    SAT-based security protocol model checker SATMC. We
    show that a symmetric key management subset of the
    Eracom PKCS#11 API, used in their ProtectServer
    product, preserves the secrecy of sensitive keys for
    unbounded numbers of fresh keys and \emph{handles},
    i.e.~pointers to keys. We also show that this API is
    not robust: if~an encryption key is lost to the
    intruder, SATMC finds an attack whereby all the keys
    may be compromised.},
    address = {York, UK},
    author = {Fr{\"o}schle, Sibylle and Steel, Graham},
    booktitle = {{R}evised {S}elected {P}apers of the {J}oint
    {W}orkshop on {A}utomated {R}easoning for {S}ecurity
    {P}rotocol {A}nalysis and {I}ssues in the {T}heory of
    {S}ecurity ({ARSPA-WITS}'09)},
    doi = {10.1007/978-3-642-03459-6_7},
    editor = {Degano, Pierpaolo and Vigan{\`o}, Luca},
    month = aug,
    pages = {92-106},
    publisher = {Springer},
    series = {Lecture Notes in Computer Science},
    title = {Analysing {PKCS}\#11 Key Management {API}s with
    Unbounded Fresh Data},
    volume = {5511},
    year = {2009},
    acronym = {{ARSPA-WITS}'09},
    nmonth = {8},
    conf-year = {2009},
    conf-month = mar,
    url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FS-arspawits09.pdf},
    pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FS-arspawits09.pdf},
    lsv-category = {intc},
    wwwpublic = {public and ccsb}
    }
  • J. Borgström, K. Bhargavan, and A. D. Gordon, “A compositional theory for STM haskell,” in 2nd acm sigplan symposium on haskell, 2009, pp. 69-80.
    [Bibtex]
    @inproceedings{BorgstromBG09,
    author = {Johannes Borgstr{\"o}m and
    Karthikeyan Bhargavan and
    Andrew D. Gordon},
    title = {A compositional theory for {STM} Haskell},
    booktitle = {2nd ACM SIGPLAN Symposium on Haskell},
    year = {2009},
    pages = {69-80},
    ee = {http://doi.acm.org/10.1145/1596638.1596648},
    bibsource = {DBLP, http://dblp.uni-trier.de}
    }
  • K. Bhargavan, R. Corin, P. Deniélou, C. Fournet, and J. J. Leifer, “Cryptographic protocol synthesis and verification for multiparty sessions,” in 22nd ieee computer security foundations symposium (csf-22), 2009, pp. 124-140.
    [Bibtex]
    @inproceedings{BhargavanCDFL09,
    author = {Karthikeyan Bhargavan and
    Ricardo Corin and
    Pierre-Malo Deni{\'e}lou and
    C{\'e}dric Fournet and
    James J. Leifer},
    title = {Cryptographic Protocol Synthesis and Verification for Multiparty
    Sessions},
    booktitle = {22nd IEEE Computer Security Foundations
    Symposium (CSF-22)},
    year = {2009},
    pages = {124-140},
    ee = {http://doi.ieeecomputersociety.org/10.1109/CSF.2009.26},
    bibsource = {DBLP, http://dblp.uni-trier.de}
    }
  • [PDF] B. Blanchet, A. D. Jaggard, J. Rao, A. Scedrov, and J. Tsay, “Refining computationally sound mechanized proofs for Kerberos,” in Workshop on formal and computational cryptography (fcc 2009), Port Jefferson, NY, 2009.
    [Bibtex]
    @inproceedings{BlanchetJaggardRaoScedrovTsayFCC09,
    author = {Bruno Blanchet and Aaron D. Jaggard and Jesse Rao and Andre Scedrov and Joe-Kai Tsay},
    title = {Refining Computationally Sound Mechanized Proofs for {K}erberos},
    booktitle = {Workshop on Formal and Computational Cryptography
    (FCC 2009)},
    year = 2009,
    address = {Port Jefferson, NY},
    month = jul,
    url = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetJaggardRaoScedrovTsayFCC09.pdf},
    pdf = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetJaggardRaoScedrovTsayFCC09.pdf}
    }

2008

  • [PDF] B. Blanchet, “Vérification automatique de protocoles cryptographiques : modèle formel et modèle calculatoire. automatic verification of security protocols: formal model and computational model,” Mémoire d’habilitation PhD Thesis, 2008.
    [Bibtex]
    @phdthesis{BlanchetHDR,
    author = {Bruno Blanchet},
    title = {V{\'e}rification automatique de protocoles cryptographiques : mod{\`e}le formel et mod{\`e}le calculatoire. Automatic verification of security protocols: formal model and computational model},
    school = {Universit{\'e} Paris-Dauphine},
    year = 2008,
    type = {M{\'e}moire d'habilitation},
    month = nov,
    url = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetHDR.pdf},
    pdf = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetHDR.pdf}
    }
  • [PDF] B. Blanchet, M. ‘i, and C. Fournet, “Automated verification of selected equivalences for security protocols,” Journal of logic and algebraic programming, vol. 75, iss. 1, p. 3–51, 2008.
    [Bibtex]
    @article{BlanchetAbadiFournetJLAP07,
    author = {Bruno Blanchet and Mart{\'\i}n Abadi and C{\'e}dric Fournet},
    title = {Automated Verification of Selected Equivalences for Security Protocols},
    journal = {Journal of Logic and Algebraic Programming},
    year = 2008,
    volume = 75,
    number = 1,
    pages = {3--51},
    month = feb # {--} # mar,
    url = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetAbadiFournetJLAP07.pdf},
    pdf = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetAbadiFournetJLAP07.pdf}
    }
  • [PDF] B. Blanchet, “A computationally sound mechanized prover for security protocols,” Ieee transactions on dependable and secure computing, vol. 5, iss. 4, p. 193–207, 2008.
    [Bibtex]
    @article{BlanchetTDSC07,
    author = {Bruno Blanchet},
    title = {A Computationally Sound Mechanized Prover for Security Protocols},
    journal = {IEEE Transactions on Dependable and Secure Computing},
    year = 2008,
    volume = 5,
    number = 4,
    pages = {193--207},
    month = oct # {--} # dec,
    url = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetTDSC07.pdf},
    pdf = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetTDSC07.pdf}
    }
  • [PDF] R. Corin, P. Deniélou, C. Fournet, K. Bhargavan, and J. J. Leifer, “A secure compiler for session abstractions,” Journal of computer security, vol. 16, iss. 5, pp. 573-636, 2008.
    [Bibtex]
    @article{CorinDFBL08,
    author = {Ricardo Corin and
    Pierre-Malo Deni{\'e}lou and
    C{\'e}dric Fournet and
    Karthikeyan Bhargavan and
    James J. Leifer},
    title = {A secure compiler for session abstractions},
    journal = {Journal of Computer Security},
    pdf = {http://prosecco.inria.fr/personal/karthik/pubs/secure-compiler-for-typed-sessions-jcs08.pdf},
    url = {http://prosecco.inria.fr/personal/karthik/pubs/secure-compiler-for-typed-sessions-jcs08.pdf},
    volume = {16},
    number = {5},
    year = {2008},
    pages = {573-636},
    ee = {http://dx.doi.org/10.3233/JCS-2008-0334},
    bibsource = {DBLP, http://dblp.uni-trier.de}
    }
  • [PDF] K. Bhargavan, C. Fournet, A. D. Gordon, and S. Tse, “Verified interoperable implementations of security protocols,” Acm transactions on programming languages and systems, vol. 31, iss. 1, 2008.
    [Bibtex]
    @article{BhargavanFGT08,
    author = {Karthikeyan Bhargavan and
    C{\'e}dric Fournet and
    Andrew D. Gordon and
    Stephen Tse},
    title = {Verified interoperable implementations of security protocols},
    journal = {ACM Transactions on Programming Languages and Systems},
    volume = {31},
    number = {1},
    year = {2008},
    pdf = {http://prosecco.inria.fr/personal/karthik/pubs/verified-interoperable-implementations-toplas08.pdf},
    url = {http://prosecco.inria.fr/personal/karthik/pubs/verified-interoperable-implementations-toplas08.pdf},
    ee = {http://doi.acm.org/10.1145/1452044.1452049},
    bibsource = {DBLP, http://dblp.uni-trier.de}
    }
  • [PDF] K. Bhargavan, C. Fournet, and A. D. Gordon, “Verifying policy-based web services security,” Acm transactions on programming languages and systems, vol. 30, iss. 6, 2008.
    [Bibtex]
    @article{BhargavanFG08,
    author = {Karthikeyan Bhargavan and
    C{\'e}dric Fournet and
    Andrew D. Gordon},
    title = {Verifying policy-based web services security},
    journal = {ACM Transactions on Programming Languages and Systems},
    volume = {30},
    number = {6},
    year = {2008},
    pdf = {http://prosecco.inria.fr/personal/karthik/pubs/verifying-policy-based-security-toplas08.pdf},
    url = {http://prosecco.inria.fr/personal/karthik/pubs/verifying-policy-based-security-toplas08.pdf},
    ee = {http://doi.acm.org/10.1145/1391956.1391957},
    bibsource = {DBLP, http://dblp.uni-trier.de}
    }
  • [PDF] B. Blanchet and A. Chaudhuri, “Automated formal analysis of a protocol for secure file sharing on untrusted storage,” in Ieee symposium on security and privacy, Oakland, CA, 2008, p. 417–431.
    [Bibtex]
    @inproceedings{BlanchetChaudhuriOakland08,
    author = {Bruno Blanchet and Avik Chaudhuri},
    title = {Automated Formal Analysis of a Protocol for Secure File Sharing on Untrusted Storage},
    booktitle = {IEEE Symposium on Security and Privacy},
    pages = {417--431},
    year = 2008,
    address = {Oakland, CA},
    month = may,
    publisher = {IEEE},
    url = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetChaudhuriOakland08.pdf},
    pdf = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetChaudhuriOakland08.pdf}
    }
  • [PDF] B. Blanchet, A. D. Jaggard, A. Scedrov, and J. Tsay, “Computationally sound mechanized proofs for basic and public-key Kerberos,” in Acm symposium on information, computer and communications security (asiaccs’08), Tokyo, Japan, 2008, p. 87–99.
    [Bibtex]
    @inproceedings{BlanchetJaggardScedrovTsayAsiaCCS08,
    author = {Bruno Blanchet and Aaron D. Jaggard and Andre Scedrov and Joe-Kai Tsay},
    title = {Computationally Sound Mechanized Proofs for Basic and Public-key {K}erberos},
    booktitle = {ACM Symposium on Information, Computer and Communications Security (ASIACCS'08)},
    pages = {87--99},
    year = 2008,
    address = {Tokyo, Japan},
    month = mar,
    publisher = {ACM},
    url = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetJaggardScedrovTsayAsiaCCS08.pdf},
    pdf = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetJaggardScedrovTsayAsiaCCS08.pdf}
    }
  • [PDF] [DOI] S. Delaune, S. Kremer, and G. Steel, “Formal analysis of PKCS\#11,” in Proceedings of the 21st IEEE Computer Security Foundations Symposium (CSF’08), Pittsburgh, PA, USA, 2008, pp. 331-344.
    [Bibtex]
    @inproceedings{DKS-csf08,
    abstract = {PKCS\#11 defines an API for cryptographic devices
    that has been widely adopted in industry. However,
    it~has been shown to be vulnerable to a variety of
    attacks that could, for example, compromise the
    sensitive keys stored on the device. In~this paper,
    we~set out a formal model of the operation of the
    API, which differs from previous security API models
    notably in that it accounts for non-monotonic mutable
    global state. We~give decidability results for our
    formalism, and describe an implementation of the
    resulting decision procedure using a model checker.
    We~report some new attacks and prove the safety of
    some configurations of the API in our model.},
    address = {Pittsburgh, PA, USA},
    author = {Delaune, St{\'e}phanie and Kremer, Steve and
    Steel, Graham},
    booktitle = {{P}roceedings of the 21st {IEEE} {C}omputer
    {S}ecurity {F}oundations {S}ymposium ({CSF}'08)},
    doi = {10.1109/CSF.2008.16},
    month = jun,
    pages = {331-344},
    publisher = {{IEEE} Computer Society Press},
    title = {Formal Analysis of {PKCS}\#11},
    year = {2008},
    acceptrate = {21/115},
    acronym = {{CSF}'08},
    nmonth = {6},
    url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKS-csf08.pdf},
    pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKS-csf08.pdf},
    longpdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2008-04.pdf},
    longps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2008-04.ps},
    lsv-category = {intc},
    wwwpublic = {public and ccsb}
    }
  • J. Bengtson, K. Bhargavan, C. Fournet, A. D. Gordon, and S. Maffeis, “Refinement types for secure implementations,” in 21st ieee computer security foundations symposium (csf-21), 2008, pp. 17-32.
    [Bibtex]
    @inproceedings{BengtsonBFGM08,
    author = {Jesper Bengtson and
    Karthikeyan Bhargavan and
    C{\'e}dric Fournet and
    Andrew D. Gordon and
    Sergio Maffeis},
    title = {Refinement Types for Secure Implementations},
    booktitle = {21st IEEE Computer Security Foundations
    Symposium (CSF-21)},
    year = {2008},
    pages = {17-32},
    ee = {http://doi.ieeecomputersociety.org/10.1109/CSF.2008.27},
    bibsource = {DBLP, http://dblp.uni-trier.de}
    }
  • K. Bhargavan, A. D. Gordon, and I. Narasamdya, “Service combinators for farming virtual machines,” in 10th international conference on coordination models and languages, 2008, pp. 33-49.
    [Bibtex]
    @inproceedings{BhargavanGN08,
    author = {Karthikeyan Bhargavan and
    Andrew D. Gordon and
    Iman Narasamdya},
    title = {Service Combinators for Farming Virtual Machines},
    booktitle = {10th International Conference on Coordination Models and Languages},
    year = {2008},
    pages = {33-49},
    ee = {http://dx.doi.org/10.1007/978-3-540-68265-3_3},
    bibsource = {DBLP, http://dblp.uni-trier.de}
    }
  • K. Bhargavan, C. Fournet, A. D. Gordon, and N. Swamy, “Verified implementations of the information card federated identity-management protocol,” in Acm symposium on information, computer and communications security (asiaccs), 2008, pp. 123-135.
    [Bibtex]
    @inproceedings{BhargavanFGS08,
    author = {Karthikeyan Bhargavan and
    C{\'e}dric Fournet and
    Andrew D. Gordon and
    Nikhil Swamy},
    title = {Verified implementations of the information card federated
    identity-management protocol},
    booktitle = {ACM Symposium on Information, Computer
    and Communications Security (ASIACCS)},
    year = {2008},
    pages = {123-135},
    ee = {http://doi.acm.org/10.1145/1368310.1368330},
    bibsource = {DBLP, http://dblp.uni-trier.de}
    }
  • K. Bhargavan, C. Fournet, R. Corin, and E. Zalinescu, “Cryptographically verified implementations for tls,” in Acm conference on computer and communications security, 2008, pp. 459-468.
    [Bibtex]
    @inproceedings{BhargavanFCZ08,
    author = {Karthikeyan Bhargavan and
    C{\'e}dric Fournet and
    Ricardo Corin and
    Eugen Zalinescu},
    title = {Cryptographically verified implementations for TLS},
    booktitle = {ACM Conference on Computer and Communications Security},
    year = {2008},
    pages = {459-468},
    ee = {http://doi.acm.org/10.1145/1455770.1455828},
    bibsource = {DBLP, http://dblp.uni-trier.de}
    }
  • [PDF] [DOI] G. Steel, “The importance of non-theorems and counterexamples in program verification,” in Revised Selected Papers and Discussions of the 1st IFIP TC2\slashWG2.3 Conference Verified Software–-Theories, Tools, and Experiments (VSTTE’05), Zurich, Switzerland, 2008, pp. 491-495.
    [Bibtex]
    @inproceedings{steel05-vstte,
    abstract = {We argue that the detection and refutation of
    non-theorems, and the discovery of appropriate
    counterexamples, is of vital importance to the Grand
    Challenge of a Program Verifier.},
    address = {Zurich, Switzerland},
    author = {Steel, Graham},
    booktitle = {{R}evised {S}elected {P}apers and {D}iscussions of
    the 1st {IFIP} {TC2}\slash{WG2.3} {C}onference
    {V}erified {S}oftware---{T}heories, {T}ools, and
    {E}xperiments ({VSTTE}'05)},
    doi = {10.1007/978-3-540-69149-5_53},
    editor = {Meyer, Bertrand and Woodcock, Jim},
    pages = {491-495},
    publisher = {Springer},
    series = {Lecture Notes in Computer Science},
    title = {The Importance of Non-theorems and Counterexamples in
    Program Verification},
    volume = {4171},
    year = {2008},
    acronym = {{VSTTE}'05},
    conf-year = {2005},
    conf-month = oct,
    url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/steel-vstte05.pdf},
    pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/steel-vstte05.pdf},
    lsv-category = {intc},
    lsv-time = {ant},
    wwwpublic = {perso}
    }

2007

  • [PDF] M. ‘i, B. Blanchet, and C. Fournet, “Just fast keying in the pi calculus,” Acm transactions on information and system security (tissec), vol. 10, iss. 3, p. 1–59, 2007.
    [Bibtex]
    @article{AbadiBlanchetFournetTISSEC07,
    author = {Mart{\'\i}n Abadi and Bruno Blanchet and C{\'e}dric Fournet},
    title = {Just Fast Keying in the Pi Calculus},
    journal = tissec,
    year = 2007,
    volume = 10,
    number = 3,
    pages = {1--59},
    month = jul,
    url = {https://bblanche.gitlabpages.inria.fr/publications/AbadiBlanchetFournetTISSEC07.pdf},
    pdf = {https://bblanche.gitlabpages.inria.fr/publications/AbadiBlanchetFournetTISSEC07.pdf}
    }
  • [PDF] K. Bhargavan, R. Corin, C. Fournet, and A. D. Gordon, “Secure sessions for web services,” Acm transactions on information and system security, vol. 10, iss. 2, 2007.
    [Bibtex]
    @article{BhargavanCFG07,
    author = {Karthikeyan Bhargavan and
    Ricardo Corin and
    C{\'e}dric Fournet and
    Andrew D. Gordon},
    title = {Secure sessions for Web services},
    journal = {ACM Transactions on Information and System Security},
    pdf = {http://prosecco.inria.fr/personal/karthik/pubs/secure-sessions-tissec07.pdf},
    url = {http://prosecco.inria.fr/personal/karthik/pubs/secure-sessions-tissec07.pdf},
    volume = {10},
    number = {2},
    year = {2007},
    ee = {http://doi.acm.org/10.1145/1237500.1237504},
    bibsource = {DBLP, http://dblp.uni-trier.de}
    }
  • [PDF] B. Blanchet, “Computationally sound mechanized proofs of correspondence assertions,” in 20th ieee computer security foundations symposium (csf’07), Venice, Italy, 2007, p. 97–111.
    [Bibtex]
    @inproceedings{BlanchetCSF07,
    author = {Bruno Blanchet},
    title = {Computationally Sound Mechanized Proofs of Correspondence Assertions},
    booktitle = {20th IEEE Computer Security Foundations Symposium (CSF'07)},
    pages = {97--111},
    year = 2007,
    address = {Venice, Italy},
    month = jul,
    organization = {IEEE},
    url = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetCSF07.pdf},
    pdf = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetCSF07.pdf}
    }
  • [PDF] [DOI] 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), Venice, Italy, 2007, pp. 79-93.
    [Bibtex]
    @inproceedings{CDS-csf07,
    abstract = {We describe a formalism for \emph{key conjuring}, the
    process by which an attacker obtains an unknown,
    encrypted key by repeatedly calling a cryptographic
    API function with random values in place of keys.
    This technique has been used to attack the security
    APIs of several Hardware Security Modules~(HSMs),
    which are widely deployed in the ATM (cash machine)
    network. We~propose a formalism for detecting
    computationally feasible key conjuring operations,
    incorporated into a Dolev-Yao style model of the
    security~API. We~show that security in the presence
    of key conjuring operations is decidable for a
    particular class of~APIs, which includes the key
    management~API of IBM's Common Cryptographic
    Architecture~(CCA).},
    address = {Venice, Italy},
    author = {Cortier, V{\'e}ronique and Delaune, St{\'e}phanie and
    Steel, Graham},
    booktitle = {{P}roceedings of the 20th {IEEE} {C}omputer
    {S}ecurity {F}oundations {S}ymposium ({CSF}'07)},
    doi = {10.1109/CSF.2007.5},
    month = jul,
    pages = {79-93},
    publisher = {{IEEE} Computer Society Press},
    title = {A Formal Theory of Key Conjuring},
    year = {2007},
    acronym = {{CSF}'07},
    nmonth = {7},
    url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDS-csf07.pdf},
    pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDS-csf07.pdf},
    ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CDS-csf07.ps},
    longpdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/RR-inria6134.pdf},
    lsv-category = {intc},
    wwwpublic = {public and ccsb}
    }
  • [PDF] [DOI] V. Cortier, G. Keighren, and G. Steel, “Automatic analysis of the security of XOR-based key management schemes,” in Proceedings of the 13th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS’07), Braga, Portugal, 2007, pp. 538-552.
    [Bibtex]
    @inproceedings{CKS-tacas07,
    abstract = {We describe a new algorithm for analysing security
    protocols that use XOR, such as key-management APIs.
    As a case study, we consider the IBM 4758 CCA API,
    which is widely used in the ATM (cash machine)
    network. Earlier versions of the CCA API were shown
    to have serious flaws, and the fixes introduced by
    IBM in version~2.41 had not previously been formally
    analysed. We first investigate IBM's proposals using
    a model checker for security protocol analysis,
    uncovering some important issues about their
    implementation. Having identified configurations we
    believed to be safe, we describe the formal
    verification of their security. We first define a new
    class of protocols, containing in particular all the
    versions of the CCA API. We then show that secrecy
    after an unbounded number of sessions is decidable
    for this class. Implementing the decision procedure
    requires some improvements, since the procedure is
    exponential. We describe a change of representation
    that leads to an implementation able to verify a
    configuration of the API in a few seconds. As a
    consequence, we obtain the first security proof of
    the fixed IBM 4758 CCA API with unbounded sessions.},
    address = {Braga, Portugal},
    author = {Cortier, V{\'e}ronique and Keighren, Gavin and
    Steel, Graham},
    booktitle = {{P}roceedings of the 13th {I}nternational
    {C}onference on {T}ools and {A}lgorithms for
    {C}onstruction and {A}nalysis of {S}ystems
    ({TACAS}'07)},
    doi = {10.1007/978-3-540-71209-1_42},
    editor = {Grumberg, Orna and Huth, Michael},
    month = mar,
    pages = {538-552},
    publisher = {Springer},
    series = {Lecture Notes in Computer Science},
    title = {Automatic Analysis of the Security of {XOR}-Based Key
    Management Schemes},
    volume = {4424},
    year = {2007},
    acceptrate = {45/170},
    acronym = {{TACAS}'07},
    nmonth = {3},
    url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CKS-tacas07.pdf},
    pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CKS-tacas07.pdf},
    lsv-category = {intc},
    lsv-time = {ant},
    wwwpublic = {perso}
    }
  • K. Bhargavan, A. D. Gordon, and I. Narasamdya, “Service combinators for farming virtual machines,” in Third symposium on trustworthy global computing (tgc), 2007, p. 22.
    [Bibtex]
    @inproceedings{BhargavanGN07,
    author = {Karthikeyan Bhargavan and
    Andrew D. Gordon and
    Iman Narasamdya},
    title = {Service Combinators for Farming Virtual Machines},
    booktitle = {Third Symposium on Trustworthy Global Computing (TGC)},
    year = {2007},
    pages = {22},
    ee = {http://dx.doi.org/10.1007/978-3-540-78663-4_3},
    bibsource = {DBLP, http://dblp.uni-trier.de}
    }
  • B. Blanchet, “CryptoVerif: a computationally sound mechanized prover for cryptographic protocols,” in Dagstuhl seminar “formal protocol verification applied”, 2007.
    [Bibtex]
    @inproceedings{BlanchetDagstuhl07,
    author = {Bruno Blanchet},
    title = {Crypto{V}erif: A Computationally Sound Mechanized Prover for Cryptographic Protocols},
    booktitle = {Dagstuhl seminar "Formal Protocol Verification Applied"},
    year = 2007,
    month = oct,
    url = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetDagstuhl07.html}
    }

2006

  • [PDF] [DOI] G. Steel, “Formal analysis of PIN block attacks,” Theoretical computer science, vol. 367, iss. 1-2, pp. 257-270, 2006.
    [Bibtex]
    @article{steel-tcs06,
    abstract = {Personal identification number (PIN) blocks are
    64-bit strings that encode a PIN ready for encryption
    and secure transmission in banking networks. These
    networks employ tamper-proof hardware security
    modules (HSMs) to perform sensitive cryptographic
    operations, such as checking the correctness of a PIN
    typed by a customer. The use of these HSMs is
    controlled by an API designed to enforce security.
    PIN block attacks are unanticipated sequences of API
    commands which allow an attacker to determine the
    value of a PIN in an encrypted PIN block. This paper
    describes a framework for formal analysis of such
    attacks. Our analysis is probabilistic, and is
    automated using constraint logic programming and
    probabilistic model checking.},
    author = {Steel, Graham},
    doi = {10.1016/j.tcs.2006.08.042},
    journal = {Theoretical Computer Science},
    month = nov,
    number = {1-2},
    pages = {257-270},
    publisher = {Elsevier Science Publishers},
    title = {Formal analysis of {PIN} block attacks},
    volume = {367},
    year = {2006},
    nmonth = {11},
    url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Steel-tcs06.pdf},
    pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Steel-tcs06.pdf},
    lsv-category = {jour},
    lsv-time = {ant},
    wwwpublic = {perso}
    }
  • [PDF] [DOI] G. Steel and A. Bundy, “Attacking group protocols by refuting incorrect inductive conjectures,” Journal of automated reasoning, vol. 36, iss. 1-2, pp. 149-176, 2006.
    [Bibtex]
    @article{SB-jar06,
    abstract = {Automated tools for finding attacks on flawed
    security protocols often fail to deal adequately with
    group protocols. The reason is that the abstractions
    made to improve performance on fixed two- or
    three-party protocols either preclude the modeling of
    group protocols altogether or permit modeling only in
    a fixed scenario, which can prevent attacks from
    being discovered. This paper describes
    \textsc{Coral}, a tool for finding counterexamples to
    incorrect inductive conjectures, which we have used
    to model protocols for both group key agreement and
    group key management, without any restrictions on the
    scenario. We show how we used \textsc{Coral} to
    discover six previously unknown attacks on three
    group protocols.},
    author = {Steel, Graham and Bundy, Alan},
    doi = {10.1007/s10817-005-9016-8},
    journal = {Journal of Automated Reasoning},
    month = jan,
    number = {1-2},
    pages = {149-176},
    publisher = {Springer},
    title = {Attacking Group Protocols by Refuting Incorrect
    Inductive Conjectures},
    volume = {36},
    year = {2006},
    nmonth = {1},
    url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/SB-jar06.pdf},
    pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/SB-jar06.pdf},
    lsv-category = {jour},
    lsv-time = {ant},
    wwwpublic = {perso}
    }
  • [PDF] B. Blanchet and D. Pointcheval, “Automated security proofs with sequences of games,” in Crypto’06, Santa Barbara, CA, 2006, p. 537–554.
    [Bibtex]
    @inproceedings{BlanchetPointchevalCrypto06,
    author = {Bruno Blanchet and David Pointcheval},
    title = {Automated Security Proofs with Sequences of Games},
    booktitle = {CRYPTO'06},
    pages = {537--554},
    year = 2006,
    editor = {Cynthia Dwork},
    volume = 4117,
    series = lncs,
    address = {Santa Barbara, CA},
    month = aug,
    publisher = spv,
    url = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetPointchevalCrypto06.pdf},
    pdf = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetPointchevalCrypto06.pdf}
    }
  • [PDF] B. Blanchet, “A computationally sound mechanized prover for security protocols,” in Ieee symposium on security and privacy, Oakland, California, 2006, pp. 140-154.
    [Bibtex]
    @inproceedings{BlanchetOakland06,
    author = {Bruno Blanchet},
    title = {A Computationally Sound Mechanized Prover for Security Protocols},
    booktitle = {IEEE Symposium on Security and Privacy},
    pages = {140-154},
    year = 2006,
    address = {Oakland, California},
    month = may,
    url = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetOakland06.pdf},
    pdf = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetOakland06.pdf}
    }
  • K. Bhargavan, C. Fournet, A. D. Gordon, and S. Tse, “Verified interoperable implementations of security protocols,” in 19th ieee computer security foundations workshop (csfw’06), 2006, p. 139–152.
    [Bibtex]
    @inproceedings{BFGT06:VerifiedInteroperableImplementationsOfSecurityProtocols,
    author = {Karthikeyan Bhargavan and C\'edric Fournet and Andrew D. Gordon and Stephen Tse},
    title = {Verified Interoperable Implementations of Security Protocols},
    booktitle = {19th IEEE Computer Security Foundations Workshop (CSFW'06)},
    pages = {139--152},
    month = Jul,
    year = 2006
    }
  • K. Bhargavan, C. Fournet, and A. D. Gordon, “Verified reference implementations of ws-security protocols,” in Third international workshop on web services and formal methods, 2006, pp. 88-106.
    [Bibtex]
    @inproceedings{BhargavanFG06,
    author = {Karthikeyan Bhargavan and
    C{\'e}dric Fournet and
    Andrew D. Gordon},
    title = {Verified Reference Implementations of WS-Security Protocols},
    booktitle = {Third International Workshop on Web Services and Formal Methods},
    year = {2006},
    pages = {88-106},
    ee = {http://dx.doi.org/10.1007/11841197_6},
    bibsource = {DBLP, http://dblp.uni-trier.de}
    }

2005

  • B. Blanchet, “Security protocols: From linear to classical logic by abstract interpretation,” Information processing letters, vol. 95, iss. 5, p. 473–479, 2005.
    [Bibtex]
    @article{BlanchetIPL05,
    author = {Bruno Blanchet},
    title = {Security Protocols: {F}rom Linear to Classical Logic by Abstract Interpretation},
    journal = ipl,
    year = 2005,
    volume = 95,
    number = 5,
    pages = {473--479},
    month = sep,
    url = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetIPL05.html}
    }
  • [PDF] B. Blanchet, M. ‘i, and C. Fournet, “Automated verification of selected equivalences for security protocols,” in 20th ieee symposium on logic in computer science (lics 2005), Chicago, IL, 2005, p. 331–340.
    [Bibtex]
    @inproceedings{BlanchetAbadiFournetLICS05,
    author = {Bruno Blanchet and Mart{\'\i}n Abadi and C{\'e}dric Fournet},
    title = {Automated Verification of Selected Equivalences for Security Protocols},
    booktitle = {20th IEEE Symposium on Logic in Computer Science (LICS 2005)},
    pages = {331--340},
    year = 2005,
    address = {Chicago, IL},
    month = jun,
    publisher = {IEEE Computer Society},
    url = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetAbadiFournetLICS05.pdf},
    pdf = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetAbadiFournetLICS05.pdf}
    }
  • [PDF] X. Allamigeon and B. Blanchet, “Reconstruction of attacks against cryptographic protocols,” in 18th ieee computer security foundations workshop (csfw-18), Aix-en-Provence, France, 2005, p. 140–154.
    [Bibtex]
    @inproceedings{AllamigeonBlanchetCSFW05,
    author = {Xavier Allamigeon and Bruno Blanchet},
    title = {Reconstruction of Attacks against Cryptographic Protocols},
    booktitle = {18th IEEE Computer Security Foundations Workshop (CSFW-18)},
    pages = {140--154},
    year = 2005,
    address = {Aix-en-Provence, France},
    month = jun,
    publisher = {IEEE Computer Society},
    url = {https://bblanche.gitlabpages.inria.fr/publications/AllamigeonBlanchetCSFW05.pdf},
    pdf = {https://bblanche.gitlabpages.inria.fr/publications/AllamigeonBlanchetCSFW05.pdf}
    }
  • [PDF] M. ‘i and B. Blanchet, “Analyzing security protocols with secrecy types and logic programs,” Journal of the acm, vol. 52, iss. 1, p. 102–146, 2005.
    [Bibtex]
    @article{AbadiBlanchetJACM7037,
    author = {Mart{\'\i}n Abadi and Bruno Blanchet},
    title = {Analyzing Security Protocols with Secrecy Types and Logic Programs},
    journal = {Journal of the ACM},
    year = 2005,
    volume = 52,
    number = 1,
    pages = {102--146},
    month = jan,
    url = {https://bblanche.gitlabpages.inria.fr/publications/AbadiBlanchetJACM7037.pdf},
    pdf = {https://bblanche.gitlabpages.inria.fr/publications/AbadiBlanchetJACM7037.pdf}
    }
  • B. Blanchet, “An automatic security protocol verifier based on resolution theorem proving (invited tutorial),” in 20th international conference on automated deduction (cade-20), Tallinn, Estonia, 2005.
    [Bibtex]
    @inproceedings{BlanchetCADE05,
    author = {Bruno Blanchet},
    title = {An Automatic Security Protocol Verifier based on Resolution Theorem Proving (invited tutorial)},
    booktitle = {20th International Conference on Automated Deduction (CADE-20)},
    year = 2005,
    address = {Tallinn, Estonia},
    month = jul,
    url = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetCADE05.html}
    }
  • B. Blanchet and A. Podelski, “Verification of cryptographic protocols: tagging enforces termination,” Theoretical computer science, vol. 333, iss. 1-2, p. 67–90, 2005.
    [Bibtex]
    @article{BlanchetPodelskiTCS04,
    author = {Bruno Blanchet and Andreas Podelski},
    title = {Verification of Cryptographic Protocols: Tagging Enforces Termination},
    journal = {Theoretical Computer Science},
    year = {2005},
    volume = {333},
    number = {1-2},
    pages = {67--90},
    month = mar,
    note = {Special issue FoSSaCS'03.},
    url = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetPodelskiTCS04.html}
    }
  • M. ‘i and B. Blanchet, “Computer-assisted verification of a protocol for certified email,” Science of computer programming, vol. 58, iss. 1–2, p. 3–27, 2005.
    [Bibtex]
    @article{AbadiBlanchetSCP04,
    author = {Mart{\'\i}n Abadi and Bruno Blanchet},
    title = {Computer-Assisted Verification of a Protocol for Certified Email},
    journal = {Science of Computer Programming},
    year = 2005,
    volume = 58,
    number = {1--2},
    pages = {3--27},
    month = oct,
    note = {Special issue SAS'03.},
    url = {https://bblanche.gitlabpages.inria.fr/publications/AbadiBlanchetSCP04.html}
    }
  • [PDF] [DOI] G. Steel, “Deduction with XOR constraints in security API modelling,” in Proceedings of the 20th International Conference on Automated Deduction (CADE’05), Tallinn, Estonia, 2005, pp. 322-336.
    [Bibtex]
    @inproceedings{steel-cade05,
    abstract = {We introduce XOR constraints, and show how they
    enable a theorem prover to reason effectively about
    security critical subsystems which employ bitwise
    XOR. Our primary case study is the API of the IBM
    4758 hardware security module. We also show how our
    technique can be applied to standard security
    protocols.},
    address = {Tallinn, Estonia},
    author = {Steel, Graham},
    booktitle = {{P}roceedings of the 20th {I}nternational
    {C}onference on {A}utomated {D}eduction ({CADE}'05)},
    doi = {10.1007/11532231_24},
    editor = {Nieuwenhuis, Robert},
    month = jul,
    pages = {322-336},
    publisher = {Springer},
    series = {Lecture Notes in Artificial Intelligence},
    title = {Deduction with {XOR} Constraints in Security {API}
    Modelling},
    volume = {3632},
    year = {2005},
    acronym = {{CADE}'05},
    nmonth = {7},
    url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/steel-cade05.pdf},
    pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/steel-cade05.pdf},
    lsv-category = {intc},
    lsv-time = {ant},
    wwwpublic = {perso}
    }

2004

  • [PDF] G. Steel, “Discovering attacks on security protocols by refuting incorrect inductive conjectures,” {Ph.}{D.} {T}hesis PhD Thesis, 2004.
    [Bibtex]
    @phdthesis{phd-steel,
    author = {Steel, Graham},
    month = may,
    school = {School of Informatics, University of Edinburgh, UK},
    type = {{Ph.}{D.} {T}hesis},
    title = {Discovering Attacks on Security Protocols by Refuting
    Incorrect Inductive Conjectures},
    year = {2004},
    nmonth = {5},
    url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/steel-these.pdf},
    pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/steel-these.pdf},
    lsv-category = {thes},
    lsv-time = {ant},
    wwwpublic = {perso}
    }
  • B. Blanchet, “Automatic proof of strong secrecy for security protocols,” in Ieee symposium on security and privacy, Oakland, California, 2004, p. 86–100.
    [Bibtex]
    @inproceedings{BlanchetOakland04,
    author = {Bruno Blanchet},
    title = {Automatic Proof of Strong Secrecy for Security Protocols},
    booktitle = {IEEE Symposium on Security and Privacy},
    pages = {86--100},
    year = {2004},
    address = {Oakland, California},
    month = may,
    url = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetOakland04.html}
    }
  • [PDF] M. ‘i, B. Blanchet, and C. Fournet, “Just fast keying in the pi calculus,” in Programming languages and systems: proceedings of the 13th european symposium on programming (ESOP’04), Barcelona, Spain, 2004, p. 340–354.
    [Bibtex]
    @inproceedings{AbadiBlanchetFournetESOP2004,
    author = {Mart{\'\i}n Abadi and Bruno Blanchet and C{\'e}dric Fournet},
    title = {Just Fast Keying in the Pi Calculus},
    booktitle = {Programming Languages and Systems: Proceedings of the
    13th European Symposium on Programming ({ESOP}'04)},
    pages = {340--354},
    year = 2004,
    editor = {David Schmidt},
    volume = 2986,
    series = lncs,
    address = {Barcelona, Spain},
    month = mar,
    publisher = spv,
    url = {https://bblanche.gitlabpages.inria.fr/publications/AbadiBlanchetFournetESOP2004.html},
    pdf = {https://bblanche.gitlabpages.inria.fr/publications/AbadiBlanchetFournetESOP2004.pdf}
    }
  • [PDF] [DOI] G. Steel, A. Bundy, and M. Maidl, “Attacking a protocol for group key agreement by refuting incorrect inductive conjectures,” in Proceedings of the 2nd International Joint Conference on Automated Reasoning (IJCAR’04), Cork, Ireland, 2004, pp. 137-151.
    [Bibtex]
    @inproceedings{SBM-ijcar04,
    abstract = {Automated tools for finding attacks on flawed
    security protocols often struggle to deal with
    protocols for group key agreement. Systems designed
    for fixed 2 or 3 party protocols may not be able to
    model a group protocol, or its intended security
    properties. Frequently, such tools require an
    abstraction to a group of fixed size to be made
    before the automated analysis takes place. This can
    prejudice chances of finding attacks on the protocol.
    In this paper, we describe \textsc{Coral}, our system
    for finding security protocol attacks by refuting
    incorrect inductive conjectures. We have used
    \textsc{Coral} to model a group key protocol in a
    general way. By posing inductive conjectures about
    the trace of messages exchanged, we can investigate
    novel properties of the protocol, such as tolerance
    to disruption, and whether it results in agreement on
    a single key. This has allowed us to find three
    distinct novel attacks on groups of size two and
    three},
    address = {Cork, Ireland},
    author = {Steel, Graham and Bundy, Alan and Maidl, Monika},
    booktitle = {{P}roceedings of the 2nd {I}nternational {J}oint
    {C}onference on {A}utomated {R}easoning ({IJCAR}'04)},
    doi = {10.1007/b98691},
    editor = {Basin, David A. and Rusinowitch, Micha{\"e}l},
    month = aug,
    pages = {137-151},
    publisher = {Springer-Verlag},
    series = {Lecture Notes in Artificial Intelligence},
    title = {Attacking a Protocol for Group Key Agreement by
    Refuting Incorrect Inductive Conjectures},
    volume = {3097},
    year = {2004},
    acronym = {{IJCAR}'04},
    nmonth = {8},
    url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/SBM-ijcar04.pdf},
    pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/SBM-ijcar04.pdf},
    lsv-category = {intc},
    lsv-time = {ant},
    wwwpublic = {perso}
    }

Comments are closed.