2023
- D. de Almeida Braga, N. Kulatova, M. Sabt, P. Fouque, and K. Bhargavan, “From Dragondoom to Dragonstar: Side-channel Attacks and Formally Verified Implementation of WPA3 Dragonfly Handshake,” in EuroS&P 2023 – IEEE 8th European Symposium on Security and Privacy, Delft, Netherlands, 2023, pp. 707-723. doi:10.1109/EuroSP57164.2023.00048
[BibTeX] [Download PDF]@inproceedings{dealmeidabraga:hal-04175322, TITLE = {{From Dragondoom to Dragonstar: Side-channel Attacks and Formally Verified Implementation of WPA3 Dragonfly Handshake}}, AUTHOR = {de Almeida Braga, Daniel and Kulatova, Natalia and Sabt, Mohamed and Fouque, Pierre-Alain and Bhargavan, Karthikeyan}, URL = {https://hal.science/hal-04175322}, NOTE = {\url{https://arxiv.org/abs/2307.09243}}, BOOKTITLE = {{EuroS\&P 2023 - IEEE 8th European Symposium on Security and Privacy}}, ADDRESS = {Delft, Netherlands}, PUBLISHER = {{IEEE}}, PAGES = {707-723}, YEAR = 2023, MONTH = Jul, DOI = {10.1109/EuroSP57164.2023.00048} } - A. Arasu, T. Ramananandro, A. Rastogi, N. Swamy, A. Fromherz, K. Hietala, B. Parno, and R. Ramamurthy, “FastVer2: A provably correct monitor for concurrent, key-value stores,” in Proceedings of the 12th ACM SIGPLAN international conference on certified programs and proofs, CPP 2023, 2023, p. 30–46.
[BibTeX] [Download PDF]@inproceedings{Arasu23, author = {Arvind Arasu and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and Aymeric Fromherz and Kesha Hietala and Bryan Parno and Ravi Ramamurthy}, editor = {Robbert Krebbers and Dmitriy Traytel and Brigitte Pientka and Steve Zdancewic}, title = {Fast{V}er2: {A} Provably Correct Monitor for Concurrent, Key-Value Stores}, booktitle = {Proceedings of the 12th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs, {CPP} 2023}, pages = {30--46}, publisher = {{ACM}}, year = {2023}, month = jan, url = {https://doi.org/10.1145/3573105.3575687} } - D. Baelde, A. Koutsos, and J. Lallemand, “A higher-order indistinguishability logic for cryptographic reasoning,” in LICS’23, 2023. doi:10.1109/LICS56636.2023.10175781
[BibTeX] [Download PDF]@inproceedings{baelde:hal-03981949, title = {A Higher-Order Indistinguishability Logic for Cryptographic Reasoning}, author = {Baelde, David and Koutsos, Adrien and Lallemand, Joseph}, url = {https://inria.hal.science/hal-03981949}, DOI = {10.1109/LICS56636.2023.10175781}, year = {2023}, booktitle = {{LICS'23}}, publisher = {{ACM}} } - M. Barbosa, G. Barthe, B. Grégoire, A. Koutsos, and P. Strub, “Mechanized proofs of adversarial complexity and application to universal composability,” ACM Transactions on Privacy and Security, vol. 26, iss. 3, pp. 1-34, 2023. doi:10.1145/3589962
[BibTeX] [Download PDF]@article{barbosa:hal-04048217, TITLE = {Mechanized Proofs of Adversarial Complexity and Application to Universal Composability}, AUTHOR = {Barbosa, Manuel and Barthe, Gilles and Gr{\'e}goire, Benjamin and Koutsos, Adrien and Strub, Pierre-Yves}, URL = {https://inria.hal.science/hal-04048217}, JOURNAL = {{ACM Transactions on Privacy and Security}}, PUBLISHER = {{ACM}}, VOLUME = 26, NUMBER = 3, PAGES = {1-34}, YEAR = 2023, MONTH = Aug, DOI = {10.1145/3589962} } - B. Blanchet, “CryptoVerif: a computationally-sound security protocol verifier (initial version with communications on channels),” Inria Paris, RR-9525, 2023.
[BibTeX] [Download PDF]@techreport{blanchet:hal-04246199, TITLE = {{CryptoVerif}: a Computationally-Sound Security Protocol Verifier (Initial Version with Communications on Channels)}, AUTHOR = {Blanchet, Bruno}, URL = {https://inria.hal.science/hal-04246199}, NOTE = {\url{https://arxiv.org/abs/2310.14658}}, NUMBER = {RR-9525}, PAGES = {166}, INSTITUTION = {Inria Paris}, YEAR = {2023}, MONTH = Oct } - B. Blanchet and C. Jacomme, “CryptoVerif: a computationally-sound security protocol verifier,” Inria, RR-9526, 2023.
[BibTeX] [Download PDF]@techreport{blanchet:hal-04253820, TITLE = {{CryptoVerif}: a Computationally-Sound Security Protocol Verifier}, AUTHOR = {Blanchet, Bruno and Jacomme, Charlie}, URL = {https://inria.hal.science/hal-04253820}, NUMBER = {RR-9526}, PAGES = {194}, INSTITUTION = {Inria}, YEAR = {2023}, MONTH = Oct } - V. Cheval and I. Rakotonirina, “Indistinguishability beyond diff-equivalence in ProVerif,” in 36th IEEE computer security foundations symposium, 2023, pp. 184-199. doi:10.1109/CSF57540.2023.00036
[BibTeX] [Download PDF]@InProceedings{ChevalCSF23b, author = {Vincent Cheval and Itsaka Rakotonirina}, title = {Indistinguishability Beyond Diff-Equivalence in {P}ro{V}erif}, booktitle = {36th {IEEE} Computer Security Foundations Symposium}, year = 2023, pages = {184-199}, month = jul, publisher = {IEEE Computer Society}, URL = {https://inria.hal.science/hal-04219230}, DOI = {10.1109/CSF57540.2023.00036} } - V. Cheval, J. Moreira, and M. Ryan, “Automatic verification of transparency protocols,” in 8th IEEE european symposium on security and privacy, EuroS&P 2023, 2023.
[BibTeX] [Download PDF]@inproceedings{CMR-EuroSnP23, author = {Vincent Cheval and Jos{\'e} Moreira and Mark Ryan}, title = {Automatic verification of transparency protocols}, booktitle = {8th {IEEE} European Symposium on Security and Privacy, {EuroS{\&}P} 2023}, month = jul, publisher = {{IEEE}}, year = {2023}, url = {https://chevalvi.gitlabpages.inria.fr/chevalvi/files/CMR-EuroSnP23.pdf} } - V. Cheval, R. Crubillé, and S. Kremer, “Symbolic protocol verification with dice : process equivalences in the presence of probabilities,” Journal of Computer Security, pp. 1-38, 2023. doi:10.3233/JCS-230037
[BibTeX] [Download PDF]@article{cheval:hal-04179875, TITLE = {Symbolic protocol verification with dice : Process equivalences in the presence of probabilities}, AUTHOR = {Cheval, Vincent and Crubill{\'e}, Rapha{\"e}lle and Kremer, Steve}, URL = {https://inria.hal.science/hal-04179875}, JOURNAL = {{Journal of Computer Security}}, PUBLISHER = {{IOS Press}}, PAGES = {1-38}, YEAR = {2023}, MONTH = Jun, DOI = {10.3233/JCS-230037} } - V. Cheval, C. Cremers, A. Dax, L. Hirschi, C. Jacomme, and S. Kremer, “Hash gone bad: automated discovery of protocol attacks that exploit hash function weaknesses,” in USENIX security ’23, 2023.
[BibTeX] [Download PDF]@inproceedings{cheval2023hash, author = {Cheval, Vincent and Cremers, Cas and Dax, Alexander and Hirschi, Lucca and Jacomme, Charlie and Kremer, Steve}, booktitle = {{USENIX} Security '23}, title = {Hash Gone Bad: Automated discovery of protocol attacks that exploit hash function weaknesses}, year = {2023}, month = aug, url = {https://charlie.jacomme.fr/publication/cheval-2023-hash/cheval-2023-hash.pdf} } - V. Cheval, V. Cortier, and A. Debant, “Election verifiability with ProVerif,” in 36th IEEE computer security foundations symposium, 2023.
[BibTeX] [Download PDF]@InProceedings{ChevalCSF23a, author = {Vincent Cheval and Véronique Cortier and Alexandre Debant}, title = {Election Verifiability with {P}ro{V}erif}, booktitle = {36th {IEEE} Computer Security Foundations Symposium}, year = {2023}, OPTpages = {}, month = jul, publisher = {IEEE Computer Society}, URL = {https://inria.hal.science/hal-04177268} } - C. Cremers, C. Jacomme, and A. Naska, “Formal analysis of session-handling in secure messaging: lifting security from sessions to conversations,” in USENIX Security ’23, 2023.
[BibTeX] [Download PDF]@inproceedings{sesame, author = {Cremers, Cas and Jacomme, Charlie and Naska, Aurora}, booktitle = {{USENIX} {S}ecurity '23}, title = {Formal Analysis of Session-Handling in Secure Messaging: Lifting Security from Sessions to Conversations}, year = {2023}, month = aug, URL = {https://hal.science/hal-03996689} } - C. Cremers, A. Dax, C. Jacomme, and M. Zhao, “Automated analysis of protocols that use authenticated encryption: how subtle AEAD differences can impact protocol security,” in USENIX security ’23, 2023.
[BibTeX] [Download PDF]@inproceedings{aead-usenix23, author = {Cremers, Cas and Dax, Alexander and Jacomme, Charlie and Zhao, Mang}, booktitle = {{USENIX} Security '23}, title = {Automated Analysis of Protocols that use Authenticated Encryption: How Subtle {AEAD} Differences can impact Protocol Security}, year = {2023}, month = aug, URL = {https://inria.hal.science/hal-04126116} } - J. Gancher, K. Sojakova, X. Fan, E. Shi, and G. Morrisett, “A core calculus for equational proofs of cryptographic protocols,” in POPL ’23: the 50th annual ACM SIGPLAN symposium on principles of programming languages, New York, NY, USA, 2023.
[BibTeX] [Download PDF]@inproceedings{10.1145/3571223, author = {Gancher, Joshua and Sojakova, Kristina and Fan, Xiong and Shi, Elaine and Morrisett, Greg}, title = {A Core Calculus for Equational Proofs of Cryptographic Protocols}, booktitle = {{POPL} '23: The 50th Annual {ACM} {SIGPLAN} Symposium on Principles of Programming Languages}, year = {2023}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, url = {https://doi.org/10.1145/3571223}, month = jan } - S. Ho, J. Protzenko, and A. Fromherz, “Aeneas: Rust verification by functional translation,” Inria Paris 2023.
[BibTeX] [Download PDF]@techreport{ho:hal-04136056, TITLE = {{Aeneas}: {Rust} Verification by Functional Translation}, AUTHOR = {Ho, Son and Protzenko, Jonathan and Fromherz, Aymeric}, URL = {https://hal.science/hal-04136056}, INSTITUTION = {Inria Paris}, YEAR = {2023}, MONTH = Apr } - S. Ho, A. Fromherz, and J. Protzenko, “Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification,” Proceedings of the ACM on Programming Languages, vol. 7, iss. ICFP, pp. 385-416, 2023. doi:10.1145/3607844
[BibTeX] [Download PDF]@article{ho:hal-04301439, TITLE = {{Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification}}, AUTHOR = {Ho, Son and Fromherz, Aymeric and Protzenko, Jonathan}, URL = {https://hal.science/hal-04301439}, JOURNAL = {{Proceedings of the ACM on Programming Languages}}, PUBLISHER = {{ACM}}, VOLUME = {7}, NUMBER = {ICFP}, PAGES = {385-416}, YEAR = {2023}, MONTH = Aug, DOI = {10.1145/3607844} } - C. Jacomme, E. Klein, S. Kremer, and M. Racouchot, “A comprehensive, formal and automated analysis of the EDHOC protocol,” in USENIX Security ’23, 2023.
[BibTeX] [Download PDF]@inproceedings{jacomme:hal-03810102, author = {Jacomme, Charlie and Klein, Elise and Kremer, Steve and Racouchot, Maïwenn}, title = {A comprehensive, formal and automated analysis of the {EDHOC} protocol}, booktitle = {{USENIX} {S}ecurity '23}, url = {https://hal.inria.fr/hal-03810102}, year = 2023, month = aug } - T. Laurent, M. Lennon-Bertrand, and K. Maillard, Definitional Functoriality for Dependent (Sub)Types, 2023.
[BibTeX] [Download PDF]@unpublished{laurent:hal-04160858, TITLE = {{Definitional Functoriality for Dependent (Sub)Types}}, AUTHOR = {Laurent, Th{\'e}o and Lennon-Bertrand, Meven and Maillard, Kenji}, URL = {https://hal.science/hal-04160858}, NOTE = {working paper or preprint}, YEAR = {2023}, MONTH = oct } - D. Merigoux, “Experience report: implementing a real-world, medium-sized program derived from a legislative specification,” in Programming languages and the law, workshop affiliated with POPL 2023, 2023.
[BibTeX] [Download PDF]@inproceedings{merigoux:hal-03869335, author = {Merigoux, Denis}, title = {Experience report: implementing a real-world, medium-sized program derived from a legislative specification}, booktitle = {Programming Languages and the Law, workshop affiliated with {POPL} 2023}, url = {https://hal.inria.fr/hal-03869335}, year = 2023, month = jan } - D. Merigoux, M. Alauzen, and L. Slimani, “Rules, Computation and Politics : Scrutinizing Unnoticed Programming Choices in French Housing Benefits,” Journal of Cross-disciplinary Research in Computational Law, vol. 1, iss. 4, 2023.
[BibTeX] [Download PDF]@article{merigoux:hal-03712130, TITLE = {{Rules, Computation and Politics : Scrutinizing Unnoticed Programming Choices in French Housing Benefits}}, AUTHOR = {Merigoux, Denis and Alauzen, Marie and Slimani, Lilya}, URL = {https://inria.hal.science/hal-03712130}, JOURNAL = {{Journal of Cross-disciplinary Research in Computational Law}}, PUBLISHER = {{OJS / PKP}}, VOLUME = {1}, NUMBER = {4}, X-TOAPPEAR_PUBDATE = {yes}, YEAR = {2023}, } - T. Wallez, “Vérification symbolique de protocoles cryptographiques en F*: application au sous-protocole TreeSync de MLS,” in JFLA 2023 – 34èmes Journées Francophones des Langages Applicatifs, Praz-sur-Arly, France, 2023, pp. 243-263.
[BibTeX] [Download PDF]@inproceedings{wallez:hal-03936726, TITLE = {{V{\'e}rification symbolique de protocoles cryptographiques en F*: application au sous-protocole TreeSync de MLS}}, AUTHOR = {Wallez, Th{\'e}ophile}, URL = {https://inria.hal.science/hal-03936726}, BOOKTITLE = {{JFLA 2023 - 34{\`e}mes Journ{\'e}es Francophones des Langages Applicatifs}}, ADDRESS = {Praz-sur-Arly, France}, EDITOR = {Timothy Bourke and Delphine Demange}, PAGES = {243-263}, YEAR = {2023}, MONTH = Jan } - T. Wallez, J. Protzenko, and K. Bhargavan, “Comparse: Provably Secure Formats for Cryptographic Protocols,” in CCS ’23: ACM SIGSAC Conference on Computer and Communications Security, Copenhagen, Denmark, 2023, pp. 564-578. doi:10.1145/3576915.3623201
[BibTeX] [Download PDF]@inproceedings{wallez:hal-04310972, TITLE = {{Comparse: Provably Secure Formats for Cryptographic Protocols}}, AUTHOR = {Wallez, Th{\'e}ophile and Protzenko, Jonathan and Bhargavan, Karthikeyan}, URL = {https://hal.science/hal-04310972}, BOOKTITLE = {{CCS '23: ACM SIGSAC Conference on Computer and Communications Security}}, ADDRESS = {Copenhagen, Denmark}, PUBLISHER = {{ACM}}, PAGES = {564-578}, YEAR = {2023}, MONTH = Nov, DOI = {10.1145/3576915.3623201} } - T. Wallez, J. Protzenko, B. Beurdouche, and K. Bhargavan, “TreeSync: authenticated group management for Messaging Layer Security,” in USENIX security ’23, 2023.
[BibTeX] [Download PDF]@InProceedings{Wallez23, author = {Théophile Wallez and Jonathan Protzenko and Benjamin Beurdouche and Karthikeyan Bhargavan}, title = {Tree{S}ync: Authenticated Group Management for {M}essaging {L}ayer {S}ecurity}, booktitle = {{USENIX} Security '23}, year = 2023, month = aug, url = {https://www.usenix.org/conference/usenixsecurity23/presentation/wallez} }
2022
- D. Baelde, S. Delaune, A. Koutsos, and S. Moreau, “Cracking the stateful nut: computational proofs of stateful security protocols using the Squirrel proof assistant,” in CSF 2022 – 35th IEEE computer security foundations symposium, 2022, p. 273–288.
[BibTeX] [Download PDF]@inproceedings{baelde:hal-03500056, author = {Baelde, David and Delaune, Stéphanie and Koutsos, Adrien and Moreau, Solène}, title = {Cracking the Stateful Nut: Computational Proofs of Stateful Security Protocols using the {S}quirrel Proof Assistant}, booktitle = {{CSF} 2022 - 35th {IEEE} Computer Security Foundations Symposium}, year = 2022, month = aug, pages = {273--288}, url = {https://hal.archives-ouvertes.fr/hal-03500056}, location = {Haifa, Israel} } - G. Barthe, A. Koutsos, S. Mirliaz, D. Pichardie, and P. Schwabe, “Semantic foundations for cost analysis of pipeline-optimized programs,” in Static analysis – 29th international symposium, SAS 2022, 2022.
[BibTeX] [Download PDF]@inproceedings{barthe:hal-03779257, author = {Barthe, Gilles and Koutsos, Adrien and Mirliaz, Solène and Pichardie, David and Schwabe, Peter}, title = {Semantic foundations for cost analysis of pipeline-optimized programs}, booktitle = {Static Analysis - 29th International Symposium, {SAS} 2022}, year = 2022, month = dec, editor = {Gagandeep Singh and Caterina Urban}, volume = 13790, series = lncs, publisher = spv, url = {https://hal.inria.fr/hal-03779257}, } - K. Bhargavan, V. Cheval, and C. Wood, “Handshake privacy for TLS 1.3 – technical report,” Inria Paris; Cloudflare 2022.
[BibTeX] [Download PDF]@TechReport{bhargavan:hal-03594482, author = {Bhargavan, Karthikeyan and Cheval, Vincent and Wood, Christopher}, title = {Handshake Privacy for {TLS} 1.3 - Technical report}, url = {https://hal.inria.fr/hal-03594482}, institution = {Inria Paris; Cloudflare}, year = 2022, month = mar } - B. Blanchet, V. Cheval, and V. Cortier, “ProVerif with lemmas, induction, fast subsumption, and much more,” in IEEE symposium on security and privacy (S&P’22), San Francisco, CA, 2022, p. 205–222.
[BibTeX] [Download PDF]@InProceedings{BlanchetEtAlSP22, author = {Blanchet, Bruno and Cheval, Vincent and Cortier, V{\'e}ronique}, title = {{P}ro{V}erif with lemmas, induction, fast subsumption, and much more}, booktitle = {{IEEE} Symposium on Security and Privacy ({S\&P}'22)}, year = 2022, pages = {205--222}, month = may, address = {San Francisco, CA}, publisher = {IEEE Computer Society}, url = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetEtAlSP22.html} } - B. Blanchet, “The security protocol verifier ProVerif and its Horn clause resolution algorithm,” Eptcs, vol. 373, p. 14–22, 2022.
[BibTeX] [Download PDF]@Article{Blanchet22, author = {Bruno Blanchet}, title = {The Security Protocol Verifier {P}ro{V}erif and its {H}orn Clause Resolution Algorithm}, journal = {EPTCS}, year = 2022, volume = 373, pages = {14--22}, month = nov, note = {G.W. Hamilton, T. Kahsai, M. Proietti (Eds.): Joint International Workshops on Horn Clauses for Verification and Synthesis (HCVS 2022) Verification and Program Transformation (VPT 2022)}, url = {https://bblanche.gitlabpages.inria.fr/publications/BlanchetHCVS22.html} } - V. Cheval, R. Crubillé, and S. Kremer, “Symbolic protocol verification with dice: process equivalences in the presence of probabilities,” in CSF’22 – 35th IEEE computer security foundations symposium, 2022, p. 319–334.
[BibTeX] [Download PDF]@inproceedings{cheval:hal-03700492, author = {Cheval, Vincent and Crubillé, Raphaëlle and Kremer, Steve}, title = {Symbolic protocol verification with dice: process equivalences in the presence of probabilities}, booktitle = {{CSF}'22 - 35th {IEEE} Computer Security Foundations Symposium}, url = {https://hal.inria.fr/hal-03700492}, pages = {319--334}, year = 2022, month = aug, location = {Haifa, Israel} } - V. Cheval, R. Crubillé, and S. Kremer, Symbolic protocol verification with dice: process equivalences in the presence of probabilities (extended version), 2022.
[BibTeX] [Download PDF]@misc{cheval:hal-03683907, author = {Cheval, Vincent and Crubillé, Raphaëlle and Kremer, Steve}, title = {Symbolic protocol verification with dice: process equivalences in the presence of probabilities (extended version)}, url = {https://hal.inria.fr/hal-03683907}, year = 2022, month = jun } - V. Cheval, C. Jacomme, S. Kremer, and R. Künnemann, “Sapic+ : protocol verifiers of the world, unite!,” in USENIX 2022 – 31st USENIX security symposium, 2022.
[BibTeX] [Download PDF]@inproceedings{cheval:hal-03693843, author = {Cheval, Vincent and Jacomme, Charlie and Kremer, Steve and Künnemann, Robert}, title = {Sapic+ : protocol verifiers of the world, unite!}, booktitle = {{USENIX} 2022 - 31st {USENIX} Security Symposium}, url = {https://hal.inria.fr/hal-03693843}, year = 2022, month = aug, location = {Boston, United States}, } - A. Delaët, D. Merigoux, and A. Fromherz, “Turning Catala into a proof platform for the law,” in Programming languages and the law, workshop affiliated with POPL 2022, 2022.
[BibTeX] [Download PDF]@inproceedings{delaet:hal-03447072, author = {Delaët, Alain and Merigoux, Denis and Fromherz, Aymeric}, title = {Turning {C}atala into a Proof Platform for the Law}, booktitle = {Programming Languages and the Law, workshop affiliated with {POPL} 2022}, url = {https://hal.inria.fr/hal-03447072}, year = 2022, month = jan } - A. Delaët and D. Merigoux, “Catala, un langage pour transformer la loi en code (démonstration),” in 33èmes journées francophones des langages applicatifs, 2022, p. 264–266.
[BibTeX] [Download PDF]@inproceedings{delaet:hal-03626853, author = {Delaët, Alain and Merigoux, Denis}, title = {Catala, un langage pour transformer la loi en code (démonstration)}, booktitle = {33èmes Journées Francophones des Langages Applicatifs}, pages = {264--266}, year = 2022, month = feb, url = {https://hal.inria.fr/hal-03626853}, } - A. Fromherz and A. Reitz, “Démonstration de steel, une logique de séparation concurrente pour prouver des programmes F* (démonstration),” in 33èmes journées francophones des langages applicatifs, 2022, p. 269–271.
[BibTeX] [Download PDF]@inproceedings{fromherz:hal-03626859, author = {Fromherz, Aymeric and Reitz, Antonin}, title = {Démonstration de Steel, une logique de séparation concurrente pour prouver des programmes {F}* (démonstration)}, booktitle = {33èmes Journées Francophones des Langages Applicatifs}, pages = {269--271}, year = 2022, month = feb, url = {https://hal.inria.fr/hal-03626859}, } - L. Huttner and D. Merigoux, “Catala: moving towards the future of legal expert systems,” Artificial intelligence and law, 2022. doi:10.1007/s10506-022-09328-5
[BibTeX] [Download PDF]@article{huttner:hal-02936606, author = {Huttner, Liane and Merigoux, Denis}, title = {Catala: Moving Towards the Future of Legal Expert Systems}, issn = {0924-8463}, eissn = {1572-8382}, journal = {Artificial Intelligence and Law}, year = 2022, month = aug, doi = {10.1007/s10506-022-09328-5}, url = {https://hal.inria.fr/hal-02936606}, publisher = spv } - D. Merigoux, M. Alauzen, and L. Slimani, Rules, computation and politics: scrutinizing unnoticed programming choices in french housing benefits, 2022.
[BibTeX] [Download PDF]@Misc{merigoux:hal-03712130, author = {Merigoux, Denis and Alauzen, Marie and Slimani, Lilya}, title = {Rules, Computation and Politics: Scrutinizing Unnoticed Programming Choices in French Housing Benefits}, url = {https://hal.inria.fr/hal-03712130}, month = dec, year = 2022 } - D. Merigoux, “Observations sur le calcul des aides au logement,” , iss. RR-9485, 2022.
[BibTeX] [Download PDF]@report{merigoux:hal-03781578, author = {Merigoux, Denis}, title = {Observations sur le calcul des aides au logement}, year = 2022, month = sep, url = {https://hal.inria.fr/hal-03781578}, institution = {Inria Paris}, number = {RR-9485}, } - D. Merigoux, The specification problem of legal expert systems, 2022.
[BibTeX] [Download PDF]@misc{merigoux:hal-03541637, author = {Merigoux, Denis}, title = {The Specification Problem of Legal Expert Systems}, url = {https://hal.inria.fr/hal-03541637}, year = 2022, month = jan }
2021
- J. Alwen, B. Blanchet, E. Hauck, E. Kiltz, B. Lipp, and D. Riepel, “Analysing the HPKE standard,” in Eurocrypt 2021, Zagreb, Croatia, 2021, p. 87–116.
[BibTeX] [Download PDF]@InProceedings{AlwenetalEurocrypt21, author = {Joël Alwen and Bruno Blanchet and Eduard Hauck and Eike Kiltz and Benjamin Lipp and Doreen Riepel}, title = {Analysing the {HPKE} Standard}, booktitle = {Eurocrypt 2021}, year = {2021}, editor = {Anne Canteaut and Francois-Xavier Standaert}, volume = {12696}, series = lncs, pages = {87--116}, month = oct, address = {Zagreb, Croatia}, publisher = spv, url = {https://bblanche.gitlabpages.inria.fr/publications/AlwenetalEurocrypt21.html} } - D. Baelde, S. Delaune, C. Jacomme, A. Koutsos, and S. Moreau, “An interactive prover for protocol verification in the computational model,” in 42nd IEEE symposium on security and privacy, SP 2021, san francisco, ca, usa, 24-27 may 2021, 2021, p. 537–554. doi:10.1109/SP40001.2021.00078
[BibTeX] [Download PDF]@inproceedings{DBLP:conf/sp/BaeldeDJKM21, author = {David Baelde and St{\'{e}}phanie Delaune and Charlie Jacomme and Adrien Koutsos and Sol{\`{e}}ne Moreau}, title = {An Interactive Prover for Protocol Verification in the Computational Model}, booktitle = {42nd {IEEE} Symposium on Security and Privacy, {SP} 2021, San Francisco, CA, USA, 24-27 May 2021}, pages = {537--554}, publisher = {{IEEE}}, year = {2021}, url = {https://doi.org/10.1109/SP40001.2021.00078}, doi = {10.1109/SP40001.2021.00078}, pdf = {https://hal.archives-ouvertes.fr/hal-03172119/document}, timestamp = {Tue, 12 Oct 2021 18:03:28 +0200}, biburl = {https://dblp.org/rec/conf/sp/BaeldeDJKM21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } - 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, pp. 777-795.
[BibTeX] [Download PDF]@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}, pages = {777-795}, month = may, publisher = {IEEE Computer Society}, url = {https://bblanche.gitlabpages.inria.fr/publications/BarbosaetalOakland21.pdf} } - M. Barbosa, G. Barthe, B. Grégoire, A. Koutsos, and P. -, “Mechanized proofs of adversarial complexity and application to universal composability,” in CCS ’21: 2021 ACM SIGSAC conference on computer and communications security, virtual event, republic of korea, november 15 – 19, 2021, 2021, p. 2541–2563. doi:10.1145/3460120.3484548
[BibTeX] [Download PDF]@inproceedings{DBLP:conf/ccs/BarbosaBGKS21, author = {Manuel Barbosa and Gilles Barthe and Benjamin Gr{\'{e}}goire and Adrien Koutsos and Pierre{-}Yves Strub}, editor = {Yongdae Kim and Jong Kim and Giovanni Vigna and Elaine Shi}, title = {Mechanized Proofs of Adversarial Complexity and Application to Universal Composability}, booktitle = {{CCS} '21: 2021 {ACM} {SIGSAC} Conference on Computer and Communications Security, Virtual Event, Republic of Korea, November 15 - 19, 2021}, pages = {2541--2563}, publisher = {{ACM}}, year = {2021}, url = {https://doi.org/10.1145/3460120.3484548}, doi = {10.1145/3460120.3484548}, pdf = {https://eprint.iacr.org/2021/156.pdf}, timestamp = {Tue, 16 Nov 2021 13:43:43 +0100}, biburl = {https://dblp.org/rec/conf/ccs/BarbosaBGKS21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } - G. Barthe, S. Cauligi, B. Grégoire, A. Koutsos, K. Liao, T. Oliveira, S. Priya, T. Rezk, and P. Schwabe, “High-assurance cryptography in the spectre era,” in 42nd IEEE symposium on security and privacy, SP 2021, san francisco, ca, usa, 24-27 may 2021, 2021, p. 1884–1901. doi:10.1109/SP40001.2021.00046
[BibTeX] [Download PDF]@inproceedings{DBLP:conf/sp/BartheCGKLOPRS21, author = {Gilles Barthe and Sunjay Cauligi and Benjamin Gr{\'{e}}goire and Adrien Koutsos and Kevin Liao and Tiago Oliveira and Swarn Priya and Tamara Rezk and Peter Schwabe}, title = {High-Assurance Cryptography in the Spectre Era}, booktitle = {42nd {IEEE} Symposium on Security and Privacy, {SP} 2021, San Francisco, CA, USA, 24-27 May 2021}, pages = {1884--1901}, publisher = {{IEEE}}, year = {2021}, url = {https://doi.org/10.1109/SP40001.2021.00046}, doi = {10.1109/SP40001.2021.00046}, pdf = {https://hal.inria.fr/hal-03352062/document}, timestamp = {Tue, 12 Oct 2021 18:03:29 +0200}, biburl = {https://dblp.org/rec/conf/sp/BartheCGKLOPRS21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } - A. Fromherz, A. Rastogi, N. Swamy, S. Gibson, G. Martínez, D. Merigoux, and T. Ramananandro, “Steel: proof-oriented programming in a dependently typed concurrent separation logic,” Proceedings of the ACM on Programming Languages, vol. 5, iss. ICFP, pp. 1-30, 2021. doi:10.1145/3473590
[BibTeX] [Download PDF]@article{fromherz:hal-03466397, TITLE = {{Steel: proof-oriented programming in a dependently typed concurrent separation logic}}, AUTHOR = {Fromherz, Aymeric and Rastogi, Aseem and Swamy, Nikhil and Gibson, Sydney and Mart{\'i}nez, Guido and Merigoux, Denis and Ramananandro, Tahina}, URL = {https://hal.inria.fr/hal-03466397}, JOURNAL = {{Proceedings of the ACM on Programming Languages}}, PUBLISHER = {{ACM}}, VOLUME = {5}, NUMBER = {ICFP}, PAGES = {1-30}, YEAR = {2021}, MONTH = Aug, DOI = {10.1145/3473590}, HAL_ID = {hal-03466397}, HAL_VERSION = {v1}, } - M. J. Gabbay, A. Jakobsson, and K. Sojakova, “Money grows on (proof-)trees: the formal FA1.2 ledger standard,” in 3rd international workshop on formal methods for blockchains, fmbc@cav 2021, july 18-19, 2021, los angeles, california, USA (virtual conference), 2021, p. 2:1–2:14.
[BibTeX] [Download PDF]@inproceedings{GJS21, author = {Murdoch James Gabbay and Arvid Jakobsson and Kristina Sojakova}, editor = {Bruno Bernardo and Diego Marmsoler}, title = {Money Grows on (Proof-)Trees: The Formal {FA1.2} Ledger Standard}, booktitle = {3rd International Workshop on Formal Methods for Blockchains, FMBC@CAV 2021, July 18-19, 2021, Los Angeles, California, {USA} (Virtual Conference)}, series = {OASIcs}, volume = {95}, pages = {2:1--2:14}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2021}, url = {https://doi.org/10.4230/OASIcs.FMBC.2021.2} } - 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} } - D. Merigoux, F. Kiefer, and K. Bhargavan, “Hacspec: succinct, executable, verifiable specifications for high-assurance cryptography embedded in Rust,” Inria, Technical Report , 2021.
[BibTeX] [Download PDF]@techreport{merigoux:hal-03176482, TITLE = {{Hacspec: succinct, executable, verifiable specifications for high-assurance cryptography embedded in Rust}}, AUTHOR = {Merigoux, Denis and Kiefer, Franziskus and Bhargavan, Karthikeyan}, URL = {https://hal.inria.fr/hal-03176482}, TYPE = {Technical Report}, INSTITUTION = {Inria}, YEAR = {2021}, MONTH = Mar, PDF = {https://hal.inria.fr/hal-03176482/file/main.pdf}, HAL_ID = {hal-03176482}, HAL_VERSION = {v1}, } - D. Merigoux, R. Monat, and J. Protzenko, “A Modern Compiler for the French Tax Code,” in CC ’21: 30th ACM SIGPLAN International Conference on Compiler Construction, Virtual, South Korea, 2021, pp. 71-82. doi:10.1145/3446804.3446850
[BibTeX] [Download PDF]@inproceedings{merigoux:hal-03002266, TITLE = {{A Modern Compiler for the French Tax Code}}, AUTHOR = {Merigoux, Denis and Monat, Rapha{\"e}l and Protzenko, Jonathan}, URL = {https://hal.inria.fr/hal-03002266}, BOOKTITLE = {{CC '21: 30th ACM SIGPLAN International Conference on Compiler Construction}}, ADDRESS = {Virtual, South Korea}, PUBLISHER = {{ACM}}, SERIES = {CC 2021: Proceedings of the 30th ACM SIGPLAN International Conference on Compiler Construction}, PAGES = {71-82}, YEAR = {2021}, MONTH = Mar, DOI = {10.1145/3446804.3446850}, KEYWORDS = {tax code ; compiler ; legal expert system}, PDF = {https://hal.inria.fr/hal-03002266v3/file/paper.pdf}, HAL_ID = {hal-03002266}, HAL_VERSION = {v3}, } - D. Merigoux, N. Chataing, and J. Protzenko, “Catala: A Programming Language for the Law,” Proceedings of the ACM on Programming Languages, vol. 5, iss. ICFP, p. 77:1-29, 2021. doi:10.1145/3473582
[BibTeX] [Download PDF]@article{merigoux:hal-03159939, TITLE = {{Catala: A Programming Language for the Law}}, AUTHOR = {Merigoux, Denis and Chataing, Nicolas and Protzenko, Jonathan}, URL = {https://hal.inria.fr/hal-03159939}, JOURNAL = {{Proceedings of the ACM on Programming Languages}}, PUBLISHER = {{ACM}}, VOLUME = {5}, NUMBER = {ICFP}, PAGES = {77:1-29}, YEAR = {2021}, MONTH = Aug, DOI = {10.1145/3473582}, PDF = {https://hal.inria.fr/hal-03159939v2/file/paper.pdf}, HAL_ID = {hal-03159939}, HAL_VERSION = {v2}, }
2020
- J. Alwen, B. Blanchet, E. Hauck, E. Kiltz, B. Lipp, and D. Riepel, Analysing the HPKE standard, 2020.
[BibTeX] [Download PDF]@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,” Proceedings of the ACM on Programming Languages, vol. 4, iss. POPL, 2020. doi:10.1145/3371072
[BibTeX] [Download PDF]@article{maillard:hal-02398927, TITLE = {The Next 700 Relational Program Logics}, AUTHOR = {Maillard, Kenji and Hritcu, Catalin and Rivas, Exequiel and van Muylder, Antoine}, URL = {https://hal.science/hal-02398927}, NOTE = {\url{https://arxiv.org/abs/1907.05244}}, JOURNAL = {{Proceedings of the ACM on Programming Languages}}, PUBLISHER = {{ACM}}, VOLUME = 4, NUMBER = {POPL}, YEAR = 2020, DOI = {10.1145/3371072} } - D. Merigoux, R. Monat, and C. Gaie, “Étude formelle de l’implémentation du code des impôts,” in JFLA 2020 – 31ème Journées Francophones des Langages Applicatifs, Gruissan, France, 2020.
[BibTeX] [Download PDF]@inproceedings{merigoux:hal-02320347, TITLE = {{{\'E}tude formelle de l'impl{\'e}mentation du code des imp{\^o}ts}}, AUTHOR = {Merigoux, Denis and Monat, Rapha{\"e}l and Gaie, Christophe}, URL = {https://inria.hal.science/hal-02320347}, BOOKTITLE = {{JFLA 2020 - 31{\`e}me Journ{\'e}es Francophones des Langages Applicatifs}}, ADDRESS = {Gruissan, France}, YEAR = 2020, MONTH = jan } - 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. doi:10.1145/3372297.3423352
[BibTeX] [Download PDF]@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} } - 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. doi:10.1109/SP40000.2020.00114
[BibTeX] [Download PDF]@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} } - Progress in cryptology – INDOCRYPT 2020 – 21st international conference on cryptology in india, bangalore, india, december 13-16, 2020, proceedingsSpringer, 2020. doi:10.1007/978-3-030-65277-7
[BibTeX] [Download PDF]@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} } - R. Blanco, M. Manighetti, and D. Miller, “FPC-Coq: Using ELPI to elaborate external proof evidence into Coq proofs,” Inria Saclay, Research Report , 2020.
[BibTeX] [Download PDF]@techreport{blanco:hal-02974002, TITLE = {{FPC-Coq: Using ELPI to elaborate external proof evidence into Coq proofs}}, AUTHOR = {Blanco, Roberto and Manighetti, Matteo and Miller, Dale}, URL = {https://inria.hal.science/hal-02974002}, TYPE = {Research Report}, INSTITUTION = {Inria Saclay}, YEAR = {2020}, MONTH = Jul } - T. Díaz, F. Olmedo, and É. Tanter, “A mechanized formalization of GraphQL,” in CPP 2020 – 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, New Orleans, United States, 2020. doi:10.1145/3372885.3373822
[BibTeX] [Download PDF]@inproceedings{diaz:hal-02422532, TITLE = {A Mechanized Formalization of {GraphQL}}, AUTHOR = {D{\'i}az, Tom{\'a}s and Olmedo, Federico and Tanter, {\'E}ric}, URL = {https://hal.science/hal-02422532}, BOOKTITLE = {{CPP 2020 - 9th ACM SIGPLAN International Conference on Certified Programs and Proofs}}, ADDRESS = {New Orleans, United States}, YEAR = {2020}, MONTH = Jan, DOI = {10.1145/3372885.3373822} } - L. Huttner and D. Merigoux, “Traduire la loi en code grâce au langage de programmation Catala,” in Intelligence artificielle et finances publiques, Nice, France, 2020.
[BibTeX] [Download PDF]@inproceedings{huttner:hal-03128248, TITLE = {{Traduire la loi en code gr{\^a}ce au langage de programmation Catala}}, AUTHOR = {Huttner, Liane and Merigoux, Denis}, URL = {https://inria.hal.science/hal-03128248}, BOOKTITLE = {{Intelligence artificielle et finances publiques}}, ADDRESS = {Nice, France}, YEAR = 2020, MONTH = oct } - S. Katsumata, E. Rivas, and T. Uustalu, “Interaction laws of monads and comonads,” in LICS ’20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken / Virtual, Germany, 2020, pp. 604-618. doi:10.1145/3373718.3394808
[BibTeX] [Download PDF]@inproceedings{katsumata:hal-03112866, TITLE = {Interaction Laws of Monads and Comonads}, AUTHOR = {Katsumata, Shin-Ya and Rivas, Exequiel and Uustalu, Tarmo}, URL = {https://inria.hal.science/hal-03112866}, BOOKTITLE = {{LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science}}, ADDRESS = {Saarbr{\"u}cken / Virtual, Germany}, PUBLISHER = {{ACM}}, PAGES = {604-618}, YEAR = {2020}, MONTH = Jul, DOI = {10.1145/3373718.3394808} } - R. Pieters, E. Rivas, and T. Schrijvers, “Generalized monoidal effects and handlers,” Journal of Functional Programming, vol. 30, 2020. doi:10.1017/S0956796820000106
[BibTeX] [Download PDF]@article{pieters:hal-03112837, TITLE = {Generalized monoidal effects and handlers}, AUTHOR = {Pieters, Ruben and Rivas, Exequiel and Schrijvers, Tom}, URL = {https://inria.hal.science/hal-03112837}, JOURNAL = {{Journal of Functional Programming}}, PUBLISHER = {{Cambridge University Press (CUP)}}, VOLUME = 30, YEAR = 2020, DOI = {10.1017/S0956796820000106} } - A. Rastogi, G. Martínez, A. Fromherz, T. Ramananandro, and N. Swamy, “Programming and proving with indexed effects,” {Microsoft Research} 2020.
[BibTeX] [Download PDF]@techreport{rastogi:hal-04256360, TITLE = {Programming and Proving with Indexed Effects}, AUTHOR = {Rastogi, Aseem and Mart{\'i}nez, Guido and Fromherz, Aymeric and Ramananandro, Tahina and Swamy, Nikhil}, URL = {https://inria.hal.science/hal-04256360}, INSTITUTION = {{Microsoft Research}}, YEAR = 2020, MONTH = oct } - N. Swamy, A. Rastogi, A. Fromherz, D. Merigoux, D. Ahman, and G. Martínez, “SteelCore: an extensible concurrent separation logic for effectful dependently typed programs,” Proceedings of the ACM on Programming Languages, vol. 4, iss. ICFP, pp. 1-30, 2020. doi:10.1145/3409003
[BibTeX] [Download PDF]@article{swamy:hal-02936273, TITLE = {{SteelCore: an extensible concurrent separation logic for effectful dependently typed programs}}, AUTHOR = {Swamy, Nikhil and Rastogi, Aseem and Fromherz, Aymeric and Merigoux, Denis and Ahman, Danel and Mart{\'i}nez, Guido}, URL = {https://inria.hal.science/hal-02936273}, NOTE = {\url{https://arxiv.org/abs/2111.15149}}, JOURNAL = {{Proceedings of the ACM on Programming Languages}}, PUBLISHER = {{ACM}}, VOLUME = {4}, NUMBER = {ICFP}, PAGES = {1-30}, YEAR = {2020}, MONTH = Aug, DOI = {10.1145/3409003} }
2019
- 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. doi:10.1109/CSF.2019.00025
[BibTeX] [Download PDF]@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 } - 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} } - 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. doi:10.4230/LIPIcs.FSTTCS.2019.1
[BibTeX] [Download PDF]@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} } - 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. doi:10.1145/3354166.3354170
[BibTeX] [Download PDF]@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} } - R. Cruz and É. Tanter, “Polymorphic relaxed noninterference,” in Proceedings of the IEEE secure development conference (secdev 2019), McLean, VA, USA, 2019, p. 101–113. doi:10.1109/SecDev.2019.00021
[BibTeX] [Download PDF]@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} } - 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. doi:10.1145/3341692
[BibTeX] [Download PDF]@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} } - C. Hritcu, “The quest for formally secure compartmentalizing compilation,” Habilitation thesis PhD Thesis, 2019.
[BibTeX] [Download PDF]@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} } - 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] [Download PDF]@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 = {The tool is available at \url{https://noiseexplorer.com/}} } - 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] [Download PDF]@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] [Download PDF]@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} } - 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. doi:10.1145/3341708
[BibTeX] [Download PDF]@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} } - 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. doi:10.1007/978-3-030-17184-1_2
[BibTeX] [Download PDF]@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] [Download PDF]@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} } - 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. doi:10.1145/3341712
[BibTeX] [Download PDF]@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} } - 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] [Download PDF]@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} } - E. Rivas and M. Jaskelioff, Monads with merging, 2019.
[BibTeX] [Download PDF]@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} } - 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. doi:10.1145/3290330
[BibTeX] [Download PDF]@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} }
2018
- 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] [Download PDF]@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}} } - 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] [Download PDF]@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} } - D. Ahman, “Handling fibred algebraic effects,” PACMPL, vol. 2, iss. {POPL}, 2018.
[BibTeX] [Download PDF]@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} } - A. Ahmed, D. Garg, C. Hritcu, and F. Piessens, “Secure Compilation (Dagstuhl Seminar 18201),” Dagstuhl reports, vol. 8, iss. 5, p. 1–30, 2018. doi:10.4230/DagRep.8.5.1
[BibTeX] [Download PDF]@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, } } - 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. doi:10.1007/978-3-319-89722-6_4
[BibTeX] [Download PDF]@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 } - K. Bhargavan, R. Barnes, and E. Rescorla, TreeKEM: Asynchronous Decentralized Key Management for Large Dynamic Groups, 2018.
[BibTeX] [Download PDF]@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} } - 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} } - B. Blanchet, “Composition theorems for CryptoVerif and application to TLS~1.3,” Inria, Research Report RR-9171, 2018.
[BibTeX] [Download PDF]@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, “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] [Download PDF]@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 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] [Download PDF]@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} } - 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. doi:10.1145/3158110
[BibTeX] [Download PDF]@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} } - 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. doi:10.1145/3192366.3192372
[BibTeX] [Download PDF]@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} } - 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. doi:10.1145/3158137
[BibTeX] [Download PDF]@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} } - 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. doi:10.1145/3167090
[BibTeX] [Download PDF]@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} } - 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. doi:10.1145/3190619.3190640
[BibTeX] [Download PDF]@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} } - H. Halpin, K. Ermoshina, and F. Musiani, Co-ordinating Developers and High-Risk Users of Privacy-Enhanced Secure Messaging Protocols, 2018.
[BibTeX] [Download PDF]@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} } - H. Halpin, Decentralizing the Social Web, 2018.
[BibTeX] [Download PDF]@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} } - M. S. New and A. Ahmed, “Graduality from embedding-projection pairs,” PACMPL, vol. 2, iss. {ICFP}, p. 73:1–73:30, 2018. doi:10.1145/3236768
[BibTeX] [Download PDF]@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} } - 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. doi:10.1007/978-3-319-89366-2_8
[BibTeX] [Download PDF]@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} } - 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. doi:10.1145/3236787
[BibTeX] [Download PDF]@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} } - M. Toro, E. Labrada, and É. Tanter, “Gradual parametricity, revisited,” Corr, vol. abs/1807.04596, 2018.
[BibTeX] [Download PDF]@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} } - 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] [Download PDF]@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} } - N. Vazou, É. Tanter, and D. V. Horn, “Gradual liquid type inference,” PACMPL, vol. 2, iss. {OOPSLA}, p. 132:1–132:25, 2018. doi:10.1145/3276502
[BibTeX] [Download PDF]@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} } - A. Weiss, D. Patterson, and A. Ahmed, “Rust distilled: an expressive tower of languages,” Corr, vol. abs/1806.02693, 2018.
[BibTeX] [Download PDF]@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} }
2017
- 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. doi:10.1145/3009837.3009878
[BibTeX] [Download PDF]@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} } - 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] [Download PDF]@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} } - 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} } - 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, B. Blanchet, and N. Kobeissi, “Verified models and reference implementations for the TLS 1.3 standard candidate,” Inria, RR-9040, 2017.
[BibTeX] [Download PDF]@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} } - 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] [Download PDF]@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} } - 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} } - 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] [Download PDF]@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] [Download PDF]@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} } - H. Halpin, “NEXTLEAP: Decentralizing Identity with Privacy for Secure Messaging,” in Proceedings of Availability, Reliability, and Security (ARES), Reggio Calabria, Italy, 2017. doi:10.1145/3098954.3104056
[BibTeX] [Download PDF]@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} } - H. Halpin and M. Piekarska, Introduction to Security and Privacy on the Blockchain, 2017.
[BibTeX] [Download PDF]@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} } - H. Halpin, “A Roadmap for High Assurance Cryptography,” in Foundations and Practice of Security, Nancy, France, 2017.
[BibTeX] [Download PDF]@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} } - 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] [Download PDF]@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} } - 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] [Download PDF]@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} } - 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. doi:10.1109/EuroSP.2017.38
[BibTeX] [Download PDF]@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} } - 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} } - 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. doi:10.1145/3009837.3009868
[BibTeX] [Download PDF]@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} } - 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. doi:10.1145/3110261
[BibTeX] [Download PDF]@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} } - 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. doi:10.1515/popets-2017-0052
[BibTeX] [Download PDF]@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} } - 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] [Download PDF]@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} } - 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] [Download PDF]@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} }
2016
- 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] [Download PDF]@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} } - 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} } - 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} } - 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} } - 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 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] [Download PDF]@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. 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} } - 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] [Download PDF]@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} } - 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] [Abstract] [Download PDF]
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.
@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} } - B. Blanchet and B. Smyth, “Automated reasoning for equivalences in the applied pi calculus with barriers,” Inria, Research report RR-8906, 2016.
[BibTeX] [Download PDF]@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}} } - 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] [Download PDF]@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}} } - H. Halpin and G. Steel, Security guidelines for cryptographic algorithms in the w3c web cryptography api, 2016.
[BibTeX] [Download PDF]@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 } - 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. doi:http://dx.doi.org/10.1017/S0956796816000058
[BibTeX] [Download PDF]@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} } - 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. doi:10.1109/CSF.2016.11
[BibTeX] [Download PDF]@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} } - 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] [Download PDF]@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} } - 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} } - M. ‘i, B. Blanchet, and C. Fournet, The applied pi calculus: mobile values, new names, and secure communication, 2016.
[BibTeX] [Abstract] [Download PDF]
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.
@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} }
2015
- 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} } - 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. doi:10.1109/SP.2015.55
[BibTeX] [Download PDF]@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} } - 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} } - 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] [Download PDF]@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} } - 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] [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.
@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.} } - 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] [Download PDF]@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/} } - 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} } - 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] [Download PDF]@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} } - 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] [Download PDF]@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 } - M. Paiola and B. Blanchet, “From the applied pi calculus to Horn clauses for protocols with lists,” Inria, Research Report RR-8823, 2015.
[BibTeX] [Abstract] [Download PDF]
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.
@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.} } - 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] [Download PDF]@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} }
2014
- 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] [Abstract] [Download PDF]
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.
@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.} } - 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. doi:10.3233/JCS-130493
[BibTeX] [Abstract] [Download PDF]
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.
@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.} } - 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)} } - 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] [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.
@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.} } - 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 } - 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} } - 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] [Download PDF]@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} } - 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 } - 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}} } - 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] [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.
@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.} } - 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] [Download PDF]@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} } - 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] [Download PDF]@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} } - 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} } - 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 } - 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] [Download PDF]@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/} } - 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 } - B. Smyth, S. Frink, and M. R. Clarkson, Election Verifiability: Definitions and an Analysis of Helios and JCJ, 2014.
[BibTeX] [Download PDF]@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/} } - B. Smyth and D. Bernhard, “Ballot secrecy with malicious bulletin boards,” Cryptology ePrint Archive, 2014/822, 2014.
[BibTeX] [Download PDF]@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 and D. Bernhard, “Ballot secrecy and ballot independence: definitions and relations,” Cryptology ePrint Archive, 2013/235, 2014.
[BibTeX] [Download PDF]@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/} } - 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] [Download PDF]@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} }
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)} } - 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] [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.
@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.} } - 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] [Download PDF]@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} } - 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] [Abstract] [Download PDF]
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.
@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} } - 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] [Abstract] [Download PDF]
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.
@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.} } - 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 } - 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] [Abstract] [Download PDF]
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.
@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} } - 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] [Abstract] [Download PDF]
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.
@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] [Abstract] [Download PDF]
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.
@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} } - 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] [Abstract] [Download PDF]
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.
@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} } - 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] [Download PDF]@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} } - 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. doi:10.1007/978-3-642-40203-6_19
[BibTeX] [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.
@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] [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.
@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} } - 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] [Abstract] [Download PDF]
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.
@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] [Abstract] [Download PDF]
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.
@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] [Abstract] [Download PDF]
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.
@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} } - 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
- 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} } - 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] [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.
@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 } - 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] [Download PDF]@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} } - 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} } - 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} } - 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} } - 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. doi:10.1145/2133375.2133378
[BibTeX] [Download PDF]@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} } - 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] [Download PDF]@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} } - 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 } - 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] [Abstract] [Download PDF]
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.
@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} } - 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] [Abstract] [Download PDF]
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.
@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} } - 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] [Abstract] [Download PDF]
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.
@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} } - 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] [Download PDF]@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} } - 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. 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. doi:10.1007/978-3-642-38004-4_17
[BibTeX] [Abstract] [Download PDF]
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.
@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} } - 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] [Abstract] [Download PDF]
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.
@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} } - 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} } - 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} } - 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} }
2011
- 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] [Download PDF]@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} } - 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] [Download PDF]@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} } - B. Blanchet, “A second look at Shoup’s lemma,” in Workshop on formal and computational cryptography (fcc 2011), Paris, France, 2011.
[BibTeX] [Download PDF]@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} } - 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] [Abstract] [Download PDF]
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.
@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} } - 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] [Abstract] [Download PDF]
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.
@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} } - 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} } - 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] [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.
@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} } - G. Steel, “Formal analysis of security APIs,” Mémoire d’habilitation PhD Thesis, 2011.
[BibTeX] [Download PDF]@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} } - 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] [Download PDF]@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} }
2010
- 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} } - 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] [Download PDF]@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} } - 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. doi:10.1145/1866307.1866337
[BibTeX] [Abstract] [Download PDF]
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.
@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} } - 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. doi:10.1007/978-3-642-15497-3_4
[BibTeX] [Abstract] [Download PDF]
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.
@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} } - 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. doi:10.3233/JCS-2009-0394
[BibTeX] [Abstract] [Download PDF]
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.
@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} } - 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. doi:10.1007/978-3-642-19751-2_8
[BibTeX] [Abstract] [Download PDF]
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.
@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} }
2009
- 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} } - B. Blanchet, “Automatic verification of correspondences for security protocols,” Journal of computer security, vol. 17, iss. 4, p. 363–434, 2009.
[BibTeX] [Download PDF]@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} } - 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] [Download PDF]@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} } - 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} } - 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. doi:10.1007/978-3-642-04444-1_4
[BibTeX] [Abstract] [Download PDF]
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.
@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} } - 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. doi:10.1007/978-3-642-04444-1_37
[BibTeX] [Abstract] [Download PDF]
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.
@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} } - 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. doi:10.1007/978-3-642-04766-4_7
[BibTeX] [Abstract] [Download PDF]
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.
@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} } - 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. doi:10.1007/978-3-642-03459-6_7
[BibTeX] [Abstract] [Download PDF]
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.
@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} } - 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. doi:10.1007/978-3-642-03459-6_12
[BibTeX] [Abstract] [Download PDF]
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.
@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} } - 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] [Download PDF]@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} }
2008
- 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, 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] [Download PDF]@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} } - 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] [Download PDF]@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} } - 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} } - 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] [Download PDF]@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} } - 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] [Download PDF]@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} } - 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] [Download PDF]@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} } - 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] [Download PDF]@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} } - 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] [Download PDF]@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} } - 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] [Download PDF]@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} } - 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. doi:10.1109/CSF.2008.16
[BibTeX] [Abstract] [Download PDF]
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.
@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} } - 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. doi:10.1007/978-3-540-69149-5_53
[BibTeX] [Abstract] [Download PDF]
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.
@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
- 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] [Download PDF]@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} } - 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, “Computationally sound mechanized proofs of correspondence assertions,” in 20th ieee computer security foundations symposium (csf’07), Venice, Italy, 2007, p. 97–111.
[BibTeX] [Download PDF]@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} } - B. Blanchet, “CryptoVerif: a computationally sound mechanized prover for cryptographic protocols,” in Dagstuhl seminar “formal protocol verification applied”, 2007.
[BibTeX] [Download PDF]@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} } - 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. doi:10.1109/CSF.2007.5
[BibTeX] [Abstract] [Download PDF]
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).
@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} } - 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. doi:10.1007/978-3-540-71209-1_42
[BibTeX] [Abstract] [Download PDF]
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.
@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} } - 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] [Download PDF]@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} }
2006
- 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} } - B. Blanchet and D. Pointcheval, “Automated security proofs with sequences of games,” in Crypto’06, Santa Barbara, CA, 2006, p. 537–554.
[BibTeX] [Download PDF]@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} } - B. Blanchet, “A computationally sound mechanized prover for security protocols,” in Ieee symposium on security and privacy, Oakland, California, 2006, pp. 140-154.
[BibTeX] [Download PDF]@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} } - G. Steel, “Formal analysis of PIN block attacks,” Theoretical computer science, vol. 367, iss. 1-2, pp. 257-270, 2006. doi:10.1016/j.tcs.2006.08.042
[BibTeX] [Abstract] [Download PDF]
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.
@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} } - 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. doi:10.1007/s10817-005-9016-8
[BibTeX] [Abstract] [Download PDF]
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.
@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} }
2005
- 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] [Download PDF]@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} } - B. Blanchet, “Security protocols: From linear to classical logic by abstract interpretation,” Information processing letters, vol. 95, iss. 5, p. 473–479, 2005.
[BibTeX] [Download PDF]@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} } - 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] [Download PDF]@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} } - 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] [Download PDF]@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] [Download PDF]@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} } - 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. doi:10.1007/11532231_24
[BibTeX] [Abstract] [Download PDF]
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.
@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} } - 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] [Download PDF]@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} } - 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] [Download PDF]@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} }
2004
- B. Blanchet, “Automatic proof of strong secrecy for security protocols,” in Ieee symposium on security and privacy, Oakland, California, 2004, p. 86–100.
[BibTeX] [Download PDF]@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} } - G. Steel, “Discovering attacks on security protocols by refuting incorrect inductive conjectures,” {Ph.}{D.} {T}hesis PhD Thesis, 2004.
[BibTeX] [Download PDF]@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} } - 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. doi:10.1007/b98691
[BibTeX] [Abstract] [Download PDF]
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
@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} } - 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] [Download PDF]@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} }
