Ph.D. student in formal modeling of safety procedures. (M/F)

Job Description

Thesis Subject

Over the last three decades, a number of models and tools have been developed and proven to be very successful in finding security flaws in communication protocols [1,2,3,4,5]. Nevertheless, while analyzing interactions within a distributed system, it is insufficient to focus solely on the technical protocol layer. Nowadays' systems involve not only computing entities (computers, servers), but also physical objects (IoT devices, smartphones, chips) and humans (users, clients) whose weaknesses and impact must be taken into account while analyzing the system's security.

To address this challenge, Ellison introduces security ceremonies that extend classical communication protocols with aspects that the latter considered out of band [6]. A ceremony brings together the system's technical and physical components as well as its users and the environment in which the system is deployed. In 2024, Fila and Radomirovic proposed a generic formal framework for specification and verification of security ceremonies [7]. This framework is suitable to model various types of agents (e.g., machines, humans, physical objects, legal rights), and supports reasoning about synchronous interactions between any finite number of agents.

The objective of this doctoral project is to continue the line of research initiated in [7] and develop a complete scientific methodology for practical analysis of security ceremonies. This includes fundamental research on modeling and analysis of ceremonies and underlying security properties, automating the verification of ceremonies, and validation of the proposed theoretical and computer tools on real-life case studies. In particular, the PhD student will address the following research challenges.

1.
Existing approaches for verification of ceremonies are based on security properties designed for protocols, e.g., secrecy, authentication, anonymity. These properties, however, do not take particularities specific to human agents and properties of physical objects into account. A study of security and functional requirements for ceremonies will be performed in order to identify and formally define properties relevant in this extended context. We aim at devising new properties involving features such as consent, intention, and origin, necessary to guarantee the expected level of security in a distributed system, from the human perspective.

2.
Numerous research attempts have shown that using tools designed for verification of protocols to analyze ceremonies is feasible but highly impractical and inefficient [7,8]. Modeling a non-deterministic behavior of humans in these tools is difficult, and the usage of non-monotonic inference rules (necessary to model the actions of forgetting, losing and recovering) poses a significant challenge for classical constraint solving algorithms. Nowar et al. have recently developed a prototype tool for ceremony verification [8]. The tool uses forward search approach, and its verification engine is inspired by graph rewriting. Preliminary tests have shown promising results regarding the tool functionality and efficiency. The PhD student will contribute to the future development of the tool. The main objective will be to extend the tool capacity in handling various types of properties (LTL, CTL, first and higher order logic formulas), and to enhance the algorithms it relies on to further improve the verification efficiency.

3.
The modeling framework from [7] and the underlying tool will be validated on real-life ceremonies, e.g., electronic voting. The goal is to identify strategies and heuristics to guide the modeler in a practical usage of the framework, research line already initiated in [9]. Modeling patterns for typical interactions with physical, security critical, and networked devices will be developed and a collection of useful contextual ceremonies will be built.


References

[1] R. Gil-Pons, R. Horne, S. Mauw, F. Stutz, S. Yurkov, Security Protocols and Threat Models -- Security and Privacy via The Applied π-Calculus. Information Security and Cryptography, Springer 2026, ISBN 978-3-032-08248-0, pp. 3-216

[2] V. Cortier, S. Kremer, Formal Models and Techniques for Analyzing Security Protocols. Cryptology and Information Security Series 5, IOS Press 2011, ISBN 978-1-60750-713-0.

[3] D. A. Basin, C. Cremers, J. Dreier, R. Sasse, Modeling and Analyzing Security Protocols with Tamarin - A Comprehensive Guide. Information Security and Cryptography, Springer 2026, ISBN 978-3-031-90935-1, pp. 3-276.

[4] D. A. Basin, C. Cremers, J. Dreier, S. Meier, R. Sasse, and
B. Schmidt. Tamarin Prover. https://tamarin-prover.github.io/

[5] B. Blanchet and V. Cheval. ProVerif: Cryptographic protocol verifier
in the formal model. Available: https://bblanche.gitlabpages.inria.fr/proverif/

[6] C. M. Ellison, Ceremony design and analysis, IACR Cryptol. 2007.

[7] B. Fila, S. Radomirovic, Nothing is out-of-band: formal modeling of ceremonies, CSF 2024: 464-478.

[8] B. Fila, N. Kazem, S. Radomirovic, Automating the verification of security ceremonies (under submission). 2026.

[9] B. Fila, E. Hoxha, Pragmatic Guidelines for Formal Modeling of Security Ceremonies. STM 2025: 43-62.

Your Work Environment

About the laboratory
=============
www.irisa.fr
IRISA is currently one of France's largest research laboratories (with over 850 staff members) in the field of computer science and information technology. Organized into seven scientific departments, IRISA is a center of excellence whose scientific priorities include bioinformatics, system security, new software architectures, virtual reality, big data analysis, and artificial intelligence. Focused on the future of computer science and inherently international in scope, IRISA is at the very heart of society's digital transition and innovation in the fields of cybersecurity, health, the environment and ecology, transportation, robotics, energy, culture, and artificial intelligence.

Presentation of the CNRS as an employer: https://www.cnrs.fr/fr/le-cnrs
Presentation of IRISA as the host laboratory: https://www.irisa.fr/umr-6074

The position falls under the Scientific and Technical Potential Protection (PPST) sector and therefore requires, in accordance with regulations, that your appointment be authorized by the competent authority at the Ministry of Higher Education, Research, and Innovation (MESR).

Translated with DeepL.com (free version)

Compensation and benefits

Compensation

2300 € gross monthly

Annual leave and RTT

44 jours

Remote Working practice and compensation

Pratique et indemnisation du TT

Transport

Prise en charge à 75% du coût et forfait mobilité durable jusqu’à 300€

About the offer

About the CNRS

The CNRS is a major player in fundamental research on a global scale. The CNRS is the only French organization active in all scientific fields. Its unique position as a multi-specialist allows it to bring together different disciplines to address the most important challenges of the contemporary world, in connection with the actors of change.

CNRS

The research professions