Bibliography
Major publications by the team in recent years
-
1D. Basin, J. Dreier, L. Hirschi, S. Radomirovic, R. Sasse, V. Stettler.
A Formal Analysis of 5G Authentication, in: ACM CCS 2018 - 25th ACM Conference on Computer and Communications Security, Toronto, Canada, Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS 2018, Toronto, ON, Canada, October 15-19, 2018, ACM Press, October 2018, vol. 14. [ DOI : 10.1145/3243734.3243846 ]
https://hal.archives-ouvertes.fr/hal-01898050 -
2W. Belkhir, Y. Chevalier, M. Rusinowitch.
Parametrized automata simulation and application to service composition, in: J. Symb. Comput., 2015, vol. 69, pp. 40–60. -
3D. Bernhard, V. Cortier, D. Galindo, O. Pereira, B. Warinschi.
A comprehensive analysis of game-based ballot privacy definitions, in: Proceedings of the 36th IEEE Symposium on Security and Privacy (S&P'15), IEEE Computer Society Press, May 2015, pp. 499–516. -
4V. Cheval, S. Kremer, I. Rakotonirina.
DEEPSEC: Deciding Equivalence Properties in Security Protocols - Theory and Practice, in: 39th IEEE Symposium on Security and Privacy, San Francisco, United States, May 2018.
https://hal.inria.fr/hal-01763122 -
5R. Chrétien, V. Cortier, S. Delaune.
Typing messages for free in security protocols: the case of equivalence properties, in: Proceedings of the 25th International Conference on Concurrency Theory (CONCUR'14), Rome, Italy, Lecture Notes in Computer Science, Springer, September 2014, vol. 8704, pp. 372-386. -
6S. Erbatur, A. M. Marshall, C. Ringeissen.
Notions of Knowledge in Combinations of Theories Sharing Constructors, in: 26th International Conference on Automated Deduction, Göteborg, Sweden, L. de Moura (editor), Lecture Notes in Artificial Intelligence, Springer, August 2017, vol. 10395, pp. 60 - 76. [ DOI : 10.1007/978-3-319-63046-5_5 ]
https://hal.inria.fr/hal-01587181 -
7H. H. Nguyen, A. Imine, M. Rusinowitch.
Anonymizing Social Graphs via Uncertainty Semantics, in: Proceedings of the 10th ACM Symposium on Information, Computer and Communications Security, (ASIA CCS'15), 2015, ACM, 2015, pp. 495–506.
Doctoral Dissertations and Habilitation Theses
-
8J. Lallemand.
Electronic Voting: Definitions and Analysis Techniques, Université de Lorraine, November 2019.
https://hal.inria.fr/tel-02396851
Articles in International Peer-Reviewed Journals
-
9R. Borgaonkar, L. Hirschi, S. Park, A. Shaik.
New Privacy Threat on 3G, 4G, and Upcoming 5G AKA Protocols, in: Proceedings on Privacy Enhancing Technologies, July 2019, vol. 2019, no 3, pp. 108-127. [ DOI : 10.2478/popets-2019-0039 ]
https://hal.inria.fr/hal-02368896 -
10P. Chocron, P. Fontaine, C. Ringeissen.
Politeness and Combination Methods for Theories with Bridging Functions, in: Journal of Automated Reasoning, 2019, forthcoming. [ DOI : 10.1007/s10817-019-09512-4 ]
https://hal.inria.fr/hal-01988452 -
11R. Chrétien, V. Cortier, A. Dallon, S. Delaune.
Typing messages for free in security protocols, in: ACM Transactions on Computational Logic, 2019, vol. 21, no 1, forthcoming. [ DOI : 10.1145/3343507 ]
https://hal.inria.fr/hal-02268400 -
12J. Dreier, L. Hirschi, S. Radomirović, R. Sasse.
Verification of Stateful Cryptographic Protocols with Exclusive OR, in: Journal of Computer Security, 2019, forthcoming.
https://hal.archives-ouvertes.fr/hal-02358878 -
13L. Hirschi, D. Baelde, S. Delaune.
A method for unbounded verification of privacy-type properties, in: Journal of Computer Security, June 2019, vol. 27, no 3, pp. 277-342. [ DOI : 10.3233/JCS-171070 ]
https://hal.inria.fr/hal-02368832 -
14L. Hirschi, R. Sasse, J. Dreier.
Security Issues in the 5G Standard and How Formal Methods Come to the Rescue, in: ERCIM News, April 2019.
https://hal.archives-ouvertes.fr/hal-02268822
Invited Conferences
-
15V. Cortier, P. Gaudry, S. Glondu.
Belenios: a simple private and verifiable electronic voting system, in: Foundations of Security, Protocols, and Equational Reasoning, Fredericksburg, Virgina, United States, J. D. Guttman, C. E. Landwehr, J. Meseguer, D. Pavlovic (editors), LNCS, Springer, 2019, vol. 11565, pp. 214-238. [ DOI : 10.1007/978-3-030-19052-1_14 ]
https://hal.inria.fr/hal-02066930
International Conferences with Proceedings
-
16B. Alipour, A. Imine, M. Rusinowitch.
Gender Inference for Facebook Picture Owners, in: TrustBus 2019 - 16th International Conference on Trust, Privacy and Security in Digital Business, Linz, Austria, S. Gritzalis, E. Weippl, S. Katsikas, G. Anderst-Kotsis, A. M. Tjoa, I. Khalil (editors), Lecture Notes in Computer Science, Springer, August 2019, vol. 11711, pp. 145–160. [ DOI : 10.1007/978-3-030-27813-7_10 ]
https://hal.univ-lorraine.fr/hal-02271825 -
17S. Anantharaman, P. Hibbs, P. Narendran, M. Rusinowitch.
Unification modulo Lists with Reverse, Relation with Certain Word Equations, in: CADE-27 - The 27th International Conference on Automated Deduction, Natal, Brazil, P. Fontaine (editor), Automated Deduction - CADE 27, Springer International Publishing, August 2019, vol. Springer-Verlag LNCS/LNAI, no 11716, pp. 1–17. [ DOI : 10.1007/978-3-030-29436-6_1 ]
https://hal.archives-ouvertes.fr/hal-02123709 -
18G. Barthe, B. Grégoire, C. Jacomme, S. Kremer, P.-Y. Strub.
Symbolic Methods in Computational Cryptography Proofs, in: CSF2019 - 32nd IEEE Computer Security Foundations Symposium, Hoboken, United States, IEEE, June 2019, pp. 136-13615. [ DOI : 10.1109/CSF.2019.00017 ]
https://hal.archives-ouvertes.fr/hal-02404701 -
19S. Bursuc, C.-C. Dragan, S. Kremer.
Private votes on untrusted platforms: models, attacks and provable scheme, in: EuroS&P 2019 - 4th IEEE European Symposium on Security and Privacy, Stockholm, Sweden, June 2019.
https://hal.inria.fr/hal-02099434 -
20S. Bursuc, S. Kremer.
Contingent payments on a public ledger: models and reductions for automated verification, in: ESORICS 2019 - The 24th European Symposium on Research in Computer Security, Luxembourg, Luxembourg, 2019.
https://hal.archives-ouvertes.fr/hal-02269063 -
21V. Cheval, S. Kremer, I. Rakotonirina.
Exploiting Symmetries When Proving Equivalence Properties for Security Protocols, in: CCS'19 - 26th ACM Conference on Computer and Communications Security, London, United Kingdom, November 2019.
https://hal.archives-ouvertes.fr/hal-02269043 -
22V. Cortier, A. Filipiak, J. Lallemand.
BeleniosVS: Secrecy and Verifiability against a Corrupted Voting Device, in: CSF 2019 - 32nd IEEE Computer Security Foundations Symposium, Hoboken, United States, June 2019.
https://hal.inria.fr/hal-02268399 -
23A. K. Eeralla, S. Erbatur, A. M. Marshall, C. Ringeissen.
Rule-Based Unification in Combined Theories and the Finite Variant Property, in: LATA 2019 - 13th International Conference on Language and Automata Theory and Applications, Saint-Petersbourg, Russia, Language and Automata Theory and Applications - 13th International Conference, LATA 2019, Proceedings., Springer, March 2019, vol. Lecture Notes in Computer Science, no 11417, pp. 356–367. [ DOI : 10.1007/978-3-030-13435-8_26 ]
https://hal.inria.fr/hal-01988419 -
24L. Hirschi, C. Cremers.
Improving Automated Symbolic Analysis of Ballot Secrecy for E-Voting Protocols: A Method Based on Sufficient Conditions, in: 2019 IEEE European Symposium on Security and Privacy (EuroS&P), Stockholm, France, IEEE, June 2019, pp. 635-650. [ DOI : 10.1109/EuroSP.2019.00052 ]
https://hal.inria.fr/hal-02368857
Scientific Books (or Scientific Book chapters)
-
25D. Basin, L. Hirschi, R. Sasse.
Symbolic Analysis of Identity-Based Protocols, in: Foundations of Security, Protocols, and Equational Reasoning, LNCS, Springer, April 2019, vol. Springer, no 11565, pp. 112-134. [ DOI : 10.1007/978-3-030-19052-1_9 ]
https://hal.inria.fr/hal-02368842 -
26M. P. Bonacina, P. Fontaine, C. Ringeissen, C. Tinelli.
Theory Combination: Beyond Equality Sharing, in: Description Logic, Theory Combination, and All That - Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday, C. Lutz, U. Sattler, C. Tinelli, A.-Y. Turhan, F. Wolter (editors), Theoretical Computer Science and General Issues, Springer, June 2019, vol. 11560, pp. 57-89.
https://hal.inria.fr/hal-02194001 -
27S. Kremer, L. Mé, D. Rémy, V. Roca.
Cybersecurity : Current challenges and Inria's research directions, Inria white book, Inria, January 2019, no 3, 172 p.
https://hal.inria.fr/hal-01993308 -
28S. Kremer, L. Mé, D. Rémy, V. Roca.
Cybersécurité : Défis actuels et axes de recherche à l'Inria, Inria white book, Inria, May 2019, no 3, 18 p.
https://hal.inria.fr/hal-02414281 -
29C. Ringeissen.
Building and Combining Matching Algorithms, in: Description Logic, Theory Combination, and All That - Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday, C. Lutz, U. Sattler, C. Tinelli, A.-Y. Turhan, F. Wolter (editors), Lecture Notes in Computer Science, Springer, June 2019, vol. 11560, pp. 523-541. [ DOI : 10.1007/978-3-030-22102-7_24 ]
https://hal.inria.fr/hal-02187244
Internal Reports
-
30S. Anantharaman, P. Hibbs, P. Narendran, M. Rusinowitch.
Unification modulo Lists with Reverse as Solving Simple Sets of Word Equations, LIFO, Université d'Orléans ; INSA, Centre Val de Loire, August 2019.
https://hal.archives-ouvertes.fr/hal-02123648 -
31V. Cortier, A. Filipiak, J. Lallemand.
BeleniosVS: Secrecy and Verifiability against a Corrupted Voting Device, CNRS, Inria, LORIA ; Orange Labs, May 2019.
https://hal.inria.fr/hal-02126077 -
32A. K. Eeralla, S. Erbatur, A. M. Marshall, C. Ringeissen.
Unification in Non-Disjoint Combinations with Forward-Closed Theories, Inria Nancy - Grand Est, 2019, no RR-9252.
https://hal.inria.fr/hal-02006179
Other Publications
-
33A. Abboud, A. Lahmadi, M. Rusinowitch, M. Couceiro, A. Bouhoula.
Minimizing Range Rules for Packet Filtering Using a Double Mask Representation, May 2019, IFIP Networking 2019, Poster.
https://hal.inria.fr/hal-02393008 -
34A. Abboud, A. Lahmadi, M. Rusinowitch, M. Couceiro, A. Bouhoula, S. E. H. Awainia, M. Ayadi.
Minimizing Range Rules for Packet Filtering Using Double Mask Representation, April 2019, working paper or preprint.
https://hal.inria.fr/hal-02102225 -
35V. Cheval, S. Kremer, I. Rakotonirina.
Exploiting symmetries when proving equivalence properties for security protocols (Technical report), 2019, working paper or preprint.
https://hal.archives-ouvertes.fr/hal-02267866 -
36V. Cortier, J. Dreier, P. Gaudry, M. Turuani.
A simple alternative to Benaloh challenge for the cast-as-intended property in Helios/Belenios, 2019, working paper or preprint.
https://hal.inria.fr/hal-02346420 -
37L. Hirschi.
Symbolic Abstractions for Quantum Protocol Verification, December 2019, https://arxiv.org/abs/1904.04186 - working paper or preprint.
https://hal.archives-ouvertes.fr/hal-02391308
-
383GPP.
Study on authentication enhancements in the 5G System (5GS), 3rd Generation Partnership Project (3GPP), no 33.846.
http://www.3gpp.org/DynaReport/33849.htm -
39M. Arapinis, L. Mancini, E. Ritter, M. Ryan, N. Golde, K. Redon, R. Borgaonkar.
New privacy issues in mobile telephony: fix and verification, in: Proc. 19th ACM Conference on Computer and Communications Security (CCS'12), ACM Press, 2012, pp. 205-216. -
40G. Barthe, F. Dupressoir, B. Grégoire, C. Kunz, B. Schmidt, P. Strub.
EasyCrypt: A Tutorial, in: Foundations of Security Analysis and Design VII - FOSAD 2012/2013 Tutorial Lectures, A. Aldini, J. López, F. Martinelli (editors), Lecture Notes in Computer Science, Springer, 2013, vol. 8604, pp. 146–166. -
41B. Blanchet.
An Efficient Cryptographic Protocol Verifier Based on Prolog Rules, in: Proc. 14th Computer Security Foundations Workshop (CSFW'01), IEEE Comp. Soc. Press, 2001, pp. 82–96. -
42B. Blanchet.
Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif, in: Foundations and Trends in Privacy and Security, 2016, vol. 1, no 1-2, pp. 1–135. -
43M. Bortolozzo, M. Centenaro, R. Focardi, G. Steel.
Attacking and Fixing PKCS#11 Security Tokens, in: Proc. 17th ACM Conference on Computer and Communications Security (CCS'10), ACM Press, 2010, pp. 260-269. -
44R. Chadha, V. Cheval, S. Ciobâcǎ, S. Kremer.
Automated verification of equivalence properties of cryptographic protocols, in: ACM Transactions on Computational Logic, 2016, vol. 17, no 4. [ DOI : 10.1145/2926715 ]
https://hal.inria.fr/hal-01306561 -
45C. Chevalier, S. Delaune, S. Kremer, M. Ryan.
Composition of Password-based Protocols, in: Formal Methods in System Design, 2013, vol. 43, pp. 369-413. -
46H. Comon-Lundh, S. Delaune.
The finite variant property: How to get rid of some algebraic properties, in: Proc. of the 16th International Conference on Rewriting Techniques and Applications (RTA'05), LNCS, Springer, 2005, vol. 3467, pp. 294-307. -
47V. Cortier, S. Delaune.
Safely Composing Security Protocols, in: Formal Methods in System Design, February 2009, vol. 34, no 1, pp. 1-36. -
48S. Delaune, S. Kremer, M. Ryan.
Verifying Privacy-type Properties of Electronic Voting Protocols, in: Journal of Computer Security, July 2009, vol. 17, no 4, pp. 435-487. -
49S. Delaune, S. Kremer, G. Steel.
Formal Analysis of PKCS#11 and Proprietary Extensions, in: Journal of Computer Security, November 2010, vol. 18, no 6, pp. 1211-1245. -
50S. Erbatur, D. Kapur, A. M. Marshall, C. Meadows, P. Narendran, C. Ringeissen.
On Asymmetric Unification and the Combination Problem in Disjoint Theories, in: Proc. 17th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'14), LNCS, Springer, 2014, pp. 274-288. -
51S. Escobar, C. Meadows, J. Meseguer.
Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties, in: Foundations of Security Analysis and Design V, LNCS, Springer, 2009, vol. 5705, pp. 1-50. -
52D. Gollmann.
What do we mean by entity authentication?, in: Proc. Symposium on Security and Privacy (SP'96), IEEE Comp. Soc. Press, 1996, pp. 46–54. -
53J. Herzog.
Applying protocol analysis to security device interfaces, in: IEEE Security & Privacy Magazine, July-Aug 2006, vol. 4, no 4, pp. 84–87. -
54B. Schmidt, S. Meier, C. Cremers, D. Basin.
The TAMARIN Prover for the Symbolic Analysis of Security Protocols, in: Proc. 25th International Conference on Computer Aided Verification (CAV'13), LNCS, Springer, 2013, vol. 8044, pp. 696-701.