Pôle Interactions Sécurité - INSPIRE

Le LMF recrute 2 professeur.e.s et 2 maître.sse.s de conférences, dont certains peuvent concerner l'activité de notre équipe. Plus d'informations sur les 4 postes ici, sur le poste de PR ENS Paris-Saclay qui peut nous concerner ici, et sur le poste de MCF Université Paris-Saclay avec profil prioritaire Sécurité ici.

La sécurité peut regrouper un grand nombre de questions. Au LMF, nous nous intéressons en particulier :

• à l'analyse automatisée de la sécurité des protocoles cryptographiques, dans des modèles symboliques ou calculatoires ;
• à la conception de protocoles cryptographiques impliquant des primitives cryptographiques avancées (chiffrement homomorphe, chiffrement fonctionnel, transfert inconscient).

Notre objectif est d'analyser des protocoles cryptographiques existants ou d'en concevoir de nouveaux, tout en étant capables d'analyser leur sécurité de manière la plus automatisée possible. Cette analyse peut permettre de prouver la sécurité ou bien de mettre en évidence des attaques. Son caractère automatisé est essentiel pour mettre en évidence des attaques complexes qu'une analyse manuelle ne permettrait pas toujours d'identifier, et pour dérouler des preuves elles aussi complexes. Parmi les deux familles de modèles de sécurité on distingue les modèles symboliques, qui offrent l'avantage d'une automatisation facilitée, mais ne permettent de simuler que des attaquants logiques, et les modèles calculatoires, qui permettent de modéliser des attaquants plus réalistes mais sont en général beaucoup plus difficiles à automatiser. Au LMF, nous nous focalisons en particulier sur le modèle de sécurité calculatoire introduit en 2012 par Bana et Comon, qui cumule deux qualités essentielles : il permet comme le modèle symbolique de dériver des règles d'inférence qui vont permettre d'automatiser les analyses, tout en modélisant des attaquants puissants et en tenant compte de l'expression de leurs capacités de calcul. C'est donc un modèle très prometteur, pour lequel nous développons un moteur d'analyse automatisé.

Ce moteur est actuellement en cours de développement, et pour le rendre pleinement efficace il nous faut encore modéliser de nombreuses primitives cryptographiques utilisées dans les protocoles, et travailler sur les mécanismes d'automatisation et de composition, qui sont loin d'être triviaux. L'intégration de techniques issues de l'analyse statique ou des solveurs SMT est notamment envisagée pour améliorer l'automatisation de cet outil. Ce travail est mené autant sur des protocoles existants que sur des protocoles de notre conception, qu'ils concernent par exemple le respect de la vie privée dans les communications 5G, dans les transactions impliquant des documents multimédia et des problématiques de droits d'auteur, ou encore dans des requêtes sur bases de données distribuées.

Au-delà de l'analyse des protocoles, nous souhaitons également à plus long terme nous pencher sur leur l'analyse de leur implémentation et pas seulement de leur spécification.

• Proving e-voting mixnets in the CCSA model: zero-knowledge proofs and rewinding, M. Catinaud, C. Fontaine, G. Scerri. preprint on HAL
• Relations among new CCA security notions for approximate FHE, S. Canard, C. Fontaine, D.-H. Phan, D. Pointcheval, M. Renard, R. Sirdey. IACR eprint 2024/812

• Automatic verification of Finite Variant Property beyond convergent equational theories, V. Cheval, C. Fontaine. 2025 IEEE 38th Computer Security Foundations Symposium (CSF 2025), pp. XX-XX, IEEE Computer Society (2025). To appear. See the extended version available on Arxiv.
• A new PET for Data Collection via Forms with Data Minimization, Full Accuracy and Informed Consent. N. Anciaux, S. Frittella, B. Joffroy, B. Nguyen, G. Scerri. 27th International Conference on Extending Database Technology (EDBT), pp.81-93 (2024)
• A Probabilistic Logic for Concrete Security, D. Baelde, C. Fontaine, A. Koutsos, G. Scerri, T. Vignon. 2024 IEEE 37th Computer Security Foundations Symposium (CSF 2024), pp. 324-339, IEEE Computer Society (2024). Also see the long version of the paper, on HAL
• A Logic and an Interactive Prover for the Computational Post-Quantum Security of Protocols, C. Cremers, C. Fontaine, C. Jacomme. 2022 IEEE Symposium on Security and Privacy (S&P), pp. 125-141, Springer-Verlag (2022). Also see the extended version available on IACR eprint archive.
• Processing Encrypted Multimedia Data Using Homomorphic Encryption, S. Canard , S. Carpov , C. Fontaine and R. Sirdey. Multimedia Security 2: Biometrics, Video Surveillance and Multimedia Encryption</a> Chapter 6, pp.173-213, Wiley (2022)
• Consent-Driven Data Use in Crowdsensing Platforms: When Data Reuse Meets Privacy-Preservation, M. Brahem, G. Scerri, N. Anciaux, and V. Issarny. In PerCom 2021 - IEEE International Conference on Pervasive Computing and Communications, Kassel / Virtual, Germany, March, 2021. HAL link
• Illuminating the Dark or how to recover what should not be seen in FE-based classifiers, S. Carpov, C. Fontaine, D. Ligier and R. Sirdey. Proceedings on Privacy Enhancing Technologies, 2020, Volume 2020, Issue 2, pp 5-23.

• BPI 2022 PQC, RESQUE project (2023-2026).  
• AMI CMA Cybersécurité, TCE project (2023-2027).  
• PEPR Cybersécurité, SVP project (2022-2028). Visit SVP web page here.