Propriété de sécurité, équivalence de processes et vérification automatique – Sequoia

L'essor d'Internet et l'omniprésence des appareils électroniques ont changé notre mode de vie. De nombreuses transactions papier se font aujourd'hui de façon numérique : services bancaires à distance, commerce et vote électronique, etc. Cette numérisation du monde comporte cependant des risques de sécurité. Des protocoles de sécurité sont déployés afin de protéger les transactions électroniques. Ce sont des programmes concurrents qui utilisent la cryptographie, p. ex. le chiffrement, afin de garantir la sécurité des données, comme la confidentialité d'un numéro de carte de crédit. Toutefois, des erreurs de conception dans ces protocoles peuvent être exploitées, et compte tenu de la nature même des services fournis, peuvent avoir des conséquences socio-économiques importantes : des élections politiques par Internet ont récemment été déployées dans plusieurs pays européens (Estonie, France, Norvège et Suisse); en France 37,7 milliards d'euros ont été dépensés en e-commerce en 2011; et des pirates visent à voler des montants toujours plus élevés (avec des transferts bancaires frauduleux dépassant 50 000 euros) en utilisant des outils d'attaque entièrement automatisés.

Ces exemples montrent l'importance de bases solides pour analyser et concevoir des protocoles de sécurité. Une approche prometteuse est l'analyse symbolique de protocoles de sécurité, basée sur des techniques de model-checking, de déduction automatique et la théorie de la concurrence. Par exemple, lors de la conception d'un modèle formel du protocole "Single Sign-On" de Google, Armando et al. ont découvert qu'un fournisseur de services malhonnête pouvait se faire passer pour un de ses utilisateurs auprès d'un autre fournisseur de services. De nombreux outils - p. ex. ProVerif , AVISPA , Scyther , FDR/CASPER ou MaudeNPA - permettent de vérifier formellement des propriétés d'authentification et de confidentialité. Cependant, les nouveaux services Internet changent à la fois les propriétés de sécurité à garantir, ainsi que les moyens mis en oeuvre. Dans des travaux récents les propriétés de respect de la vie privée s'expriment comme des propriétés d'indistinguabilité. L'indistinguabilité permet de modéliser un large éventail de propriétés de sécurité et exprime que l'adversaire est incapable de distinguer entre deux situations, et se modélise naturellement en termes d'équivalences dans des calculs de processus cryptographiques.

Cependant, la plupart des outils d'analyse de protocoles sont limités aux propriétés d'accessibilité, e.g., l'authentification et des formes faibles de confidentialité, alors que de nombreuses propriétés de sécurité (en particulier les propriétés de respect de la vie privée, telles que l'anonymat et la non-traçabilité) s'expriment en termes d'équivalences. D'où la nécessité de nouveaux outils et techniques capables d'analyser ces propriétés d'équivalence. Les objectifs de ce projet sont
- d'étudier quelles notions d'équivalences - parmi la multitude d'équivalence existantes - sont appropriées pour une propriété de sécurité donnée, pour refléter un système et des capacités de l'attaquant;
- d'avancer l'état de l'art de la vérification automatique des équivalences de processus, en permettant par exemple plus de primitives cryptographiques, motivées par des études de cas;
- d'étudier des protocoles qui utilisent des secrets faibles, par exemple, les protocoles d'authentification multi-facteurs. Nous pensons que les propriétés de sécurité relatives à la présence de ces secrets faibles peuvent être naturellement exprimées comme des équivalences de processus;
- d'appliquer ces résultats à des études de cas dans le vote électronique. Des protocoles récents visent à limiter la confiance dans l'ordinateur utilisé pour voter, en utilisant des secrets faibles, et sont hors de portée des techniques d'analyse actuelles.