The Information Technology Security Evaluation Facility (ITSEF) conducts activities in the field of security evaluation of electronic systems, embedded software components, either within the framework of certification schemes, for example the one led by the l’Agence Nationale de la Sécurité des Systèmes d’information (ANSSI), or at the direct request of developers.
In the context of security evaluations conducted by the ITSEF, evaluators are required, among other things, to test the resistance of cryptographic mechanisms embedded on smart cards against physical attacks, such as chip tampering attacks or attacks by observing compromising signals. In an application context (banking, healthcare, identity), these mechanisms are used within cryptographic protocols, such as key exchanges or authentications. When a vulnerability is detected in a product, the evaluator must analyze its impact on the protocol. Currently, this analysis relies on the evaluator's expertise, but the use of formal methods would be advantageous for tracing attack paths or for providing greater assurance that the vulnerability will not be exploited.
Initially, this thesis will focus on studying existing verification tools (e.g., Tamarin [1]) in order to test them on the protocols used in commonly evaluated applications. The thesis will then aim to examine the different ways in which a vulnerability can be expressed within the protocol, and to evaluate the tool's ability to formally analyze its impacts by identifying attack paths. Finally, the PhD student will be required to enhance the tool with new components to address the identified needs.
References
[1] Tamarin : https://github.com/tamarin-prover/tamarin-prover