Sites Inria

English version

Algorithmique, programmation, logiciels et architectures

30/08/2011

Apporter des réponses pour des échanges plus sûrs

© Inria / Photo Kaksonen © Inria / Photo Kaksonen

Vérifier des protocoles cryptographiques, présents dans le commerce en ligne ou les distributeurs de billets, mais aussi mettre en place des outils de détection d’intrusion dans un système informatique, et ainsi alerter si une suite d’actions semblent malveillantes, tels sont les objectifs de l’équipe-projet Secsi (commune avec le LSV, le CNRS, et l’ENS Cachan). À l’occasion de la soutenance de l’habilitation à diriger des recherches (HDR) de trois de ses membres, focus sur leurs travaux de recherche.

Stéphanie Delaune : « Dans les outils de protection de l’anonymat, tout est à construire »

© Inria / Photo Kaksonen

Notre identité, et les informations nous concernant, se retrouvent sur de nombreux supports, et sont pour cela protéger par des protocoles cryptographiques. Commerce en ligne, carte bancaire… nous pensons connaître les situations où les échanges cryptés nous protègent. Pourtant, de nouvelles failles sont découvertes régulièrement, et demandent d’élargir notre recherche . Qui imaginerait par exemple que la personne assise à côté de vous à l’aéroport puisse connaître votre identité grâce à la puce de votre passeport ? L’électronique est de plus en plus présent, et induit des échanges d’informations qu’il nous faut protéger. Les voitures de demain qui communiqueront entre elles, sur les bouchons et distances de sécurité, ne devront pas livrer à des personnes malveillantes votre adresse ou vos habitudes de conduite. Ces nouvelles applications posent de nouvelles problématiques.
Jusqu'à maintenant, je m'étais beaucoup consacrée aux problèmes de confidentialité et d'authentification dans des applications comme celles présentes dans le commerce en ligne ou les distributeurs de billets. Mais aujourd’hui, notre identité numérique se démultiplie. Or les techniques mathématiques de vérification ne peuvent pas s’appliquer telles quelles de la confidentialité à la protection de l’anonymat : il faut adapter, tout est à construire. Le respect de la vie privée demandera de plus en plus de protection.
Et pour la suite ?  : Responsable de l’ANR VIP (Vérification de propriétés d'indistinguabilité) qui démarre en janvier 2012.

Steve Kremer : « Les mathématiques nous permettent de rapprocher notre protocole du modèle réel »

Les protocoles de sécurité sont censés apporter confidentialité, authentification et anonymat. Ils sont utilisés dans des domaines de plus en plus divers, comme récemment dans le domaine du vote électronique. En Europe en 2011, les votes pour les élections parlementaires de Suisse et d’Estonie, ainsi que les élections municipales et régionales en Norvège, ont pu se faire par internet.

© Inria / Photo Kaksonen

Notre travail est de formaliser et d’analyser de façon automatique des protocoles de sécurité . C’est-à-dire que nous devons modéliser le protocole, l’écrire en langage mathématique, formel, puis décrire exactement ce qu’on veut dire par ses différentes propriétés. Sur l’exemple du vote électronique, la notion d’anonymat semble assez claire au premier abord. Mais si le vote est unanime, on saura qui a voté quoi… Il faut donc être très précis pour couvrir toutes les situations. Nous veillons à ce qu’un attaquant ne puisse pas avoir des informations sur les votes, mais également qu’un votant ne puisse pas divulguer son vote : l’anonymat ne peut pas être « cassé », même si on le souhaite.
Plus récemment, je me suis concentré sur la correction calculatoire de nos modèles. Comme je viens de l’expliquer, nous commençons par modéliser le protocole pour ensuite le vérifier, mais pour cela on s’éloigne du programme réellement exécuté. L’attaquant est par exemple idéalisé, puisque l’on définit les actions qu’il peut exécuter. Il reste donc toujours un risque que l’on rate des attaques qui seraient en dehors du modèle. Avec les cryptographes, la description du protocole va être plus précise, et l’attaquant pourra par exemple deviner des secrets, ou exécuter des algorithmes arbitraires. Les preuves pourront ainsi être plus fortes, dans un modèle plus précis qui comprendra plus d’attaques a priori.
Et pour la suite ?  : Intégration au 1er septembre 2011 de l’équipe-projet Cassis au centre Nancy - Grand-Est .

Graham Steel : « Nous essayons de définir un nouveau standard de sécurité pour les cartes à puces »

© Inria / Photo Kaksonen

Toutes les cartes à puces utilisent une interface de programmation particulière appelée API. Le système est construit pour que la clé cryptographique ne sorte jamais de la carte : elle peut crypter et décrypter, mais tout se fait en interne. L’API correspond donc à l’ensemble des commandes d’exécution qui peuvent être envoyées à la carte à puces.
Depuis 26 ans, l’API le plus utilisé est le PKCS 11, qui est appliqué notamment dans les banques. Depuis 2003, il a été prouvé, d’abord manuellement puis en 2008 grâce à la vérification avec un model checker, que des attaques sur ce modèle étaient possibles. Mais corriger les failles de sécurité n’est pas si simple quand on sait que l’implémentation de ce modèle standard peut être très variable, et que chaque situation peut donc impliquer des attaques différentes … En effet, il est très difficile de réaliser une configuration sûre à partir de PKCS 11.
Nous avons donc commencé par suggérer des changements dans les modèles pour supprimer petit à petit des types d’attaques particuliers. Nous souhaitions affiner le modèle. Mais du coup, nous avons commencé à concevoir un nouveau standard avec un niveau de sécurité beaucoup plus fort, et qui offre moins de variations dans l’implémentation pour limiter les risques. En effet, on n’essaie pas seulement de casser des protocoles, mais aussi de construire de nouvelles solutions. Nous espérons ainsi proposer bientôt un modèle plus facile à utiliser.

Mots-clés : Sécurité Secsi Cryptographie Saclay - Île-de-France

Haut de page

Suivez Inria