Vérification de propriétés d'indistinguabilité pour les protocoles cryptographiques ; Verification of indistinguishability properties for cryptographic protocols
You can manage bookmarks using lists, please log in to your user account for this.
Media type:
Text;
E-Book;
Electronic Thesis
Title:
Vérification de propriétés d'indistinguabilité pour les protocoles cryptographiques ; Verification of indistinguishability properties for cryptographic protocols
Footnote:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Description:
Cette thèse s'inscrit dans le domaine de la vérification de protocoles cryptographiques dans le modèle symbolique. Plus précisément, il s'agit de s'assurer à l'aide de méthodes formelles que de petits programmes distribués satisfont à des propriétés d'indistinguabilité, c'est-à-dire qu'un attaquant n'est pas capable de deviner quelle situation (parmi deux)il observe. Ce formalisme permet d'exprimer des propriétés de sécurité comme le secret fort, l'intraçabilité ou l'anonymat. De plus, les protocoles sont exécutés simultanément par un grand nombre d'agents, à plusieurs reprises si bien que nous nous heurtons très rapidement à des résultats d'indécidabilité. Dès lors, il faut ou bien tenir compte du nombre arbitraire de sessions et rechercher des méthodes de semi-décision ou identifier des classes décidables ;ou bien établir des procédures de décision pour un nombre fini de sessions. Au moment où nous avons commencé les travaux présentés dans cette thèse les outils de vérification de propriétés d'indistinguabilité pour un nombre borné de sessions ne permettaient de traiter que très peu de sessions :dans certains cas il était tout juste possible de modéliser un échange complet. Cette thèse présente des procédures de décision efficaces dans ce cadre. Dans un premier temps, nous établissons des résultats de petite attaque. Pour des protocoles déterministes nous démontrons qu'il existe une attaque si, et seulement s’il existe une attaque bien typée lorsque toute confusion entre les types des variables est évitée. De plus, nous prouvons que, lorqu'il existe une attaque l'attaquant peut la trouver en utilisant au plus trois constantes. Dans un second temps, nous traduisons le problème d'indistinguabilité en termes d'accessibilité dans un système de planification qui est résolu par l'algorithme du graphe de planification associé à un codage SAT. Nous terminons en confirmant l'efficacité de la démarche ,à travers l'implémentation de l'outil SAT-Equivet sa comparaison vis-à-vis des outils analogues. ; This thesis presents ...