Publications of the ERC project SPOOC
• 2020 • 2019 • 2018 • 2017 • 2016 •
2020
- Kushal Babel, Vincent Cheval, and Steve Kremer. On the semantics of communications when verifying equivalence properties. Journal of Computer Security, 28(1):71–127, 2020.
doi:10.3233/JCS-191366
Details BibTeX Download: [pdf] [HTML] - Gilles Barthe, Charlie Jacomme, and Steve Kremer. Universal equivalence and majority on probabilistic programs over finite fields. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS'20), pp. 155–166, ACM, Saarbrücken, July 2020.
doi:10.1145/3373718.3394746
Details BibTeX Download: [pdf (long version)] [HTML] - Vincent Cheval, Steve Kremer, and Itsaka Rakotonirina. The hitchhiker's guide to decidability and complexity of equivalence properties in security protocols. In Logic, Language, and Security. Essays Dedicated to Andre Scedrov on the Occasion of His 65th Birthday, Lecture Notes in Computer Science 12300, Springer, 2020.
doi:10.1007/978-3-030-62077-6_10
Details BibTeX Download: [pdf] [pdf (long version)] [HTML] - Rémy Chrétien, Véronique Cortier, Antoine Dallon, and Stéphanie Delaune. Typing messages for free in security protocols. ACM Transactions on Computational Logic, 21(1):1–52, 2020.
doi:10.1145/3343507
Details BibTeX Download: [pdf] [HTML] - Véronique Cortier, Joseph Lallemand, and Bogdan Warinschi. Fifty Shades of Ballot Privacy: Privacy against a Malicious Board. In 33rd IEEE Computer Security Foundations Symposium (CSF'20), Boston, USA, June 2020. Distinguished paper award.
doi:10.1109/CSF49147.2020.00010
Details BibTeX Download: [pdf] [pdf (long version)] [HTML] - Véronique Cortier, Stéphanie Delaune, and Jannik Dreier. Automatic generation of sources lemmas in Tamarin: towards automatic proofs of security protocols. In 25th European Symposium on Research in Computer Security (ESORICS 2020), pp. 3–22, Lecture Notes in Computer Science 12309, Guilford, United Kingdom, September 2020. Best paper award.
doi:10.1007/978-3-030-59013-0_1
Details BibTeX Download: [pdf] [HTML]
2019
- Gilles Barthe, Benjamin Grégoire, Charlie Jacomme, Steve Kremer, and Pierre-Yves Strub. Symbolic Methods in Computational Cryptography Proofs. In Proceedings of the 32nd IEEE Computer Security Foundations Symposium (CSF'19), pp. 136–151, IEEE Computer Society Press, Hoboken, NJ, USA, June 2019.
doi:10.1109/CSF.2019.00017
Details BibTeX Download: [pdf] [pdf (long version)] [HTML] - Sergiu Bursuc and Steve Kremer. Contingent payments on a public ledger: models and reductions for automated verification. In Proceedings of the 24th European Symposium on Research in Computer Security, Part I (ESORICS'19), pp. 361–382, Lecture Notes in Computer Science 11735, Springer, Luxembourg, September 2019.
doi:10.1007/978-3-030-29959-0_18
Details BibTeX Download: [pdf] [HTML] - Sergiu Bursuc, Constantin-Cătălin Drăgan, and Steve Kremer. Private votes on untrusted platforms: models, attacks and provable scheme. In Proceedings of the 4th IEEE European Symposium on Security and Privacy (EuroS&P'19), IEEE Computer Society Press, Stockholm, Sweden, June 2019.
doi:10.1109/EuroSP.2019.00050
Details BibTeX Download: [pdf] [HTML] - Vincent Cheval, Steve Kremer, and Itsaka Rakotonirina. Exploiting Symmetries When Proving Equivalence Properties for Security Protocols. In Proceedings of the 26th ACM Conference on Computer and Communications Security (CCS'19), pp. 905–922, ACM, London, UK, November 2019.
doi:10.1145/3319535.3354260
Details BibTeX Download: [pdf] [pdf (long version)] [HTML] - Véronique Cortier, Alicia Filipiak, and Joseph Lallemand. BeleniosVS: Secrecy and Verifiability against a Corrupted Voting Device. In 32nd IEEE Computer Security Foundations Symposium (CSF'19), pp. 367–381, IEEE Computer Society Press, Hoboken, June 2019.
Details BibTeX Download: [pdf] - Ajay Kumar Eeralla, Serdar Erbatur, Andrew M. Marshall, and Christophe Ringeissen. Rule-Based Unification in Combined Theories and the Finite Variant Property. In 13th International Conference on Language and Automata Theory and Applications (LATA'19), pp. 356–367, Lecture Notes in Computer Science 11417, Springer, 2019.
doi:10.1007/978-3-030-13435-8_26
Details BibTeX Download: [pdf] [HTML]
2018
- David A. Basin, Jannik Dreier, Lucca Hirschi, Sasa Radomirovic, Ralf Sasse, and Vincent Stettler. A Formal Analysis of 5G Authentication. In 25th ACM Conference on Computer and Communications Security (CCS'18), pp. 1383–1396, ACM, 2018.
doi:10.1145/3243734.3243846
Details BibTeX Download: [pdf] [HTML] - Vincent Cheval, Véronique Cortier, and Mathieu Turuani. A little more conversation, a little less action, a lot more satisfaction: Global states in ProVerif. In Proceedings of the 31st IEEE Computer Security Foundations Symposium (CSF'18), pp. 344–358, IEEE Computer Society Press, July 2018.
doi:10.1109/CSF.2018.00032
Details BibTeX Download: [pdf] [pdf (long version)] [HTML] - Vincent Cheval, Steve Kremer, and Itsaka Rakotonirina. DEEPSEC: Deciding Equivalence Properties in Security Protocols - Theory and Practice. In Proceedings of the 39th IEEE Symposium on Security and Privacy (S&P'18), pp. 525–542, IEEE Computer Society Press, San Francisco, CA, USA, May 2018. Distinguished paper award.
doi:10.1109/SP.2018.00033
Details BibTeX Download: [pdf] [pdf (long version)] [HTML] - Vincent Cheval, Steve Kremer, and Itsaka Rakotonirina. The DEEPSEC prover. In Proceedings of the 30th International Conference on Computer Aided Verification, Part II (CAV'18), Springer, Oxford, UK, July 2018.
doi:10.1007/978-3-319-96142-2_4
Details BibTeX Download: [pdf] [HTML] - Véronique Cortier and Joseph Lallemand. Voting: You Can't Have Privacy without Individual Verifiability. In 25th ACM Conference on Computer and Communications Security (CCS'18), pp. 53–66, ACM, 2018.
doi:10.1145/3243734.3243762
Details BibTeX Download: [pdf] [HTML] - Véronique Cortier, Constantin Catalin Dragan, Pierre-Yves Strub, Francois Dupressoir, and Bogdan Warinschi. Machine-checked proofs for electronic voting: privacy and verifiability for Belenios. In Proceedings of the 31st IEEE Computer Security Foundations Symposium (CSF'18), pp. 298–312, IEEE Computer Society Press, July 2018.
doi:10.1109/CSF.2018.00029
Details BibTeX Download: [pdf] [HTML] - Véronique Cortier, Stéphanie Delaune, and Antoine Dallon. Efficiently deciding equivalence for standard primitives and phases. In Proceedings of the 23rd European Symposium on Research in Computer Security, Part I (ESORICS'18), pp. 491–511, Lecture Notes in Computer Science 11098, Springer, September 2018.
doi:10.1007/978-3-319-99073-6_24
Details BibTeX Download: [pdf] [HTML] - Véronique Cortier, Niklas Grimm, Joseph Lallemand, and Matteo Maffei. Equivalence properties by typing in cryptographic branching protocols. In Proceedings of the 7th International Conference on Principles of Security and Trust (POST'18), pp. 160–187, April 2018.
doi:https://doi.org/10.1007/978-3-319-89722-6_7
Details BibTeX Download: [pdf] [HTML] - Véronique Cortier, David Galindo, and Mathieu Turuani. A formal analysis of the Neuchâtel e-voting protocol. In 3rd IEEE European Symposium on Security and Privacy (EuroSP'18), London, UK, April 2018.
doi:10.1109/EuroSP.2018.00037
Details BibTeX Download: [pdf] [HTML] - Charlie Jacomme and Steve Kremer. An extensive formal analysis of multi-factor authentication protocols. In Proceedings of the 31st IEEE Computer Security Foundations Symposium (CSF'18), IEEE Computer Society Press, Oxford, UK, July 2018. To appear.
Details BibTeX Download: (unavailable)
2017
- Kushal Babel, Vincent Cheval, and Steve Kremer. On communication models when verifying equivalence properties. In Proceedings of the 6th International Conference on Principles of Security and Trust (POST'17), pp. 141–163, Springer, Uppsala, Sweden, April 2017.
Details BibTeX Download: [pdf] - Kushal Babel, Vincent Cheval, and Steve Kremer. On communication models when verifying equivalence properties. In Proceedings of the 6th International Conference on Principles of Security and Trust (POST'17), pp. 141–163, Lecture Notes in Computer Science 10204, Springer, Uppsala, Sweden, April 2017.
doi:10.1007/978-3-662-54455-6
Details BibTeX Download: [pdf] [pdf (long version)] [HTML] - Michael Backes, Jannik Dreier, Steve Kremer, and Robert Künnemann. A Novel Approach for Reasoning about Liveness in Cryptographic Protocols and its Application to Fair Exchange. In Proceedings of the 2nd IEEE European Symposium on Security and Privacy (EuroS&P'17), pp. 76–91, IEEE Computer Society, Paris, France, April 2017.
Details BibTeX Download: [pdf] - David Baelde, Stéphanie Delaune, Ivan Gazeau, and Steve Kremer. Symbolic verification of privacy-type properties for security protocols with XOR. In Proceedings of the 30th IEEE Computer Security Foundations Symposium (CSF'17), IEEE Computer Society Press, Santa Barbara, USA, August 2017.
Details BibTeX Download: [pdf] [pdf (long version)] - Vincent Cheval, Véronique Cortier, and Bogdan Warinschi. Secure composition of PKIs with public key protocols. In Proceedings of the 30th IEEE Computer Security Foundations Symposium (CSF'17), IEEE Computer Society Press, August 2017.
Details BibTeX Download: [pdf] - Véronique Cortier, Stéphanie Delaune, and Antoine Dallon. SAT-Equiv: an efficient tool for equivalence properties. In Proceedings of the 30th IEEE Computer Security Foundations Symposium (CSF'17), IEEE Computer Society Press, August 2017.
Details BibTeX Download: [pdf] - Véronique Cortier, Alicia Filipiak, Jan Florent, Said Gharout, and Jacques Traoré. Designing and proving an EMV-compliant payment protocol for mobile devices. In Proceedings of the 2nd IEEE European Symposium on Security and Privacy (EuroS&P'17), pp. 467–480, IEEE Computer Society, Paris, France, April 2017.
Details BibTeX Download: [pdf] - Stéphanie Delaune, Steve Kremer, and Ludovic Robin. Formal verification of protocols based on short authenticated strings. In Proceedings of the 30th IEEE Computer Security Foundations Symposium (CSF'17), IEEE Computer Society Press, Santa Barbara, USA, August 2017.
Details BibTeX Download: [pdf] [pdf (long version)] - Serdar Erbatur, Andrew M. Marshall, and Christophe Ringeissen. Notions of Knowledge in Combinations of Theories Sharing Constructors. In Proceedings of 26th International Conference on Automated Deduction (CADE'17), Lecture Notes in Computer Science, Springer, Gothenburg, Sweden, August 2017.
doi:10.1007/978-3-319-63046-5
Details BibTeX Download: [HTML] - Ivan Gazeau and Steve Kremer. Automated analysis of equivalence properties for security protocols using else branches. In Proceedings of the 22nd European Symposium on Research in Computer Security (ESORICS'17), Lecture Notes in Computer Science, Springer, Oslo, Norway, September 2017.
Details BibTeX Download: [pdf] [pdf (long version)] - Charlie Jacomme, Steve Kremer, and Guillaume Scerri. Symbolic Models for Isolated Execution Environments. In Proceedings of the 2nd IEEE European Symposium on Security and Privacy (EuroS&P'17), pp. 530–545, IEEE Computer Society, Paris, France, April 2017.
Details BibTeX Download: [pdf] [pdf (long version)]
2016
- Myrto Arapinis, Véronique Cortier, and Steve Kremer. When are three voters enough for privacy properties?. In Proceedings of the 21st European Symposium on Research in Computer Security (ESORICS'16), pp. 241–260, Lecture Notes in Computer Science 9879, Springer, Heraklion, Crete, September 2016.
doi:10.1007/978-3-319-45741-3_13
Details BibTeX Download: [pdf] [pdf (long version)] [HTML] - Rohit Chadha, Vincent Cheval, Ștefan Ciobâcă, and Steve Kremer. Automated verification of equivalence properties of cryptographic protocol. ACM Transactions on Computational Logic, 17(4):1–32, November 2016.
doi:10.1145/2926715
Details BibTeX Download: [pdf] [HTML] - Pyrros Chaidos, Véronique Cortier, Georg Fuchsbauer, and David Galindo. BeleniosRF: A Non-interactive Receipt-Free Electronic Voting Scheme. In 23rd ACM Conference on Computer and Communications Security (CCS'16), ACM, Vienna, Austria, October 2016.
doi:10.1145/2976749.2978337
Details BibTeX Download: [pdf] [HTML] - Steve Kremer and Peter Rønne. To Du or not to Du: A Security Analysis of Du-Vote. In Proceedings of the 1st IEEE European Symposium on Security and Privacy (EuroS&P'16), pp. 303–323, IEEE Computer Society, Saarbrücken, Germany, March 2016.
doi:10.1109/EuroSP.2016.42
Details BibTeX Download: [pdf] [HTML] - Steve Kremer and Robert Künnemann. Automated analysis of security protocols with global state. Journal of Computer Security, 24(5):583–616, IOS Press, 2016.
doi:10.3233/JCS-160556
Details BibTeX Download: [pdf] [HTML] - Mathieu Turuani, Thomas Voegtlin, and Michael Rusinowitch. Automated Verification of Electrum Wallet. In 3rd Workshop on Bitcoin and Blockchain Research, Christ Church, Barbados, February 2016.
doi:0.1007/978-3-662-53357-4_3
Details BibTeX Download: [pdf] [HTML]