Projet ANR-10-VERS-0004 – ProSe : Protocoles de sécurité : modèle formel, modèle calculatoire et implémentations
Programme : RESEAUX DU FUTUR ET SERVICES (VERSO) 2010
Année de financement : 2010
Coordinateur du projet : Monsieur Bruno BLANCHET (INRIA Paris- Rocquencourt)
Partenaires : Laboratoire Spécification et Vérification; Combinaison d'Approches pour la Sécurité des Systèmes Infinis; Inria Centre Paris - Rocquencourt; Laboratoire Verimag
Montant : 434576.0 euros
Durée : 48 mois
Résumé : Aujourd'hui, une quantité énorme d'informations transite par des canaux qui ne sont pas sûrs. Et cela va encore augmenter significativement dans le futur. Les réseaux mobiles de capteurs sont déployés partout et contrôlent de plus en plus d'activités dans la société: la conduite automobile, la santé, le trafic, le contrôle de production.... Les réseaux mobiles et les réseaux ad-hoc, la téléphonie mobile, et plus généralement les terminaux mobiles, sont de plus en plus utilisés dans la vie quotidienne. Les puces sont utilisées pour stocker des données sensibles et sont censées sécuriser des transactions critiques: elles sont embarquées dans les passeports électroniques, les cartes de santé, les cartes bancaires. Et, bien sûr, l'utilisation d'Internet se répand, depuis les services bancaires électroniques, l'achat en ligne, jusqu'aux nouveaux domaines d'applications, comme le partage de données (P2P), l'informatique de confiance et le vote électronique, constituant ainsi de nouvelles menaces.
Sécuriser les communications est par conséquent un défi et un enjeu majeurs.
La communauté scientifique en informatique a déployé beaucoup d'efforts pour essayer de sécuriser les communications. Elle a aussi
déployé beaucoup d'efforts pour tenter d'accroître notre confiance, en produisant des ``preuves de sécurité''. De telles preuves nécessitent un cadre formel pour les protocoles, pour les propriétés de sécurité et pour décrire l'attaquant supposé. Jusqu'en 2001 plusieurs communautés de recherche ont travaillé indépendamment sur ce sujet, en utilisant des modèles formels différents.  Parmi ces approches, citons d'abord l'approche
logique (ou symbolique) des protocoles et de leur analyse, dont le succès peut être illustré par les nombres attaques du type ``man-in-the-middle'' qui ont été découvertes à partir de 1995 sur la plupart des protocoles publiés à cette époque. Citons ensuite une approche calculatoire, ou computationnelle, qui s'appuie sur la théorie de la complexité; elle suppose par exemple que l'attaquant est une machine de Turing randomisée quelconque, dont le temps de calcul est polynomial. Il s'agit du modèle favori en cryptologie. Une troisième approche est plus pragmatique et tente de prouver/trouver des attaques sur des programmes réalisant les protocoles. En fait, cette approche n'a pas permis beaucoup de preuves de protocoles jusqu'à présent, mais a permis de trouver des attaques.
Le principal objectif du projet ProSe est de permettre d'obtenir des preuves de sécurité à plusieurs niveaux: symbolique, calculatoire, programmes.
Il s'agit donc de développer des outils pour la preuve automatique de protocoles dans le modèle symbolique, dans le modèle calculatoire, dans un modèle de programmes. Pour cela, le projet s'appuiera sur l'expérience déjà acquise par les participants dans le domaine des preuves symboliques et  du lien entre preuves symboliques et calculatoires.