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.