Approximations pour la vérification automatique de protocoles de sécurité
Institution:
BesançonDisciplines:
Directors:
Abstract EN:
Secured communications are the foundations of on-line critical applications as e-commerce, e-voting, etc. Automatically verifying such secured communications, represented as security protocols, is of the first interest for industrials. By representing the secrecy verification problem as the reachability problem in rewriting, we propose to automate a method, initially dedicated to expert users, verifying secrecy properties on approximations of the intruder knowledge. The intruder knowledge is a set of terms computed from a given one (representing the initial intruder's knowledge) using a term rewriting system (specifying the intruder and the security protocol). By a semi-algorithm, we provide a diagnostic mentioning that a secrecy property is either violated thanks to the computation of an under-estimation of the intruder knowledge, or satisfied with the computation of an over-estimation. This semi-algorithm is implemented in the automatic TA4SP tool. This tool is integrated in the AVISPA tool (http://www. Avispa-project. Org), a tool-set dedicated to automatic verification of security protocols. We also proposed a technique to reconstruct proof trees of terms reachability in approximated context meaning that attack traces can be drawn as soon as a secrecy property is violated.
Abstract FR:
Cette thèse s’inscrit dans le cadre de la vérification de systèmes critiques. Le problème de sécurité consiste à déterminer si un système est sûr ou non et également pourquoi il ne l’est pas. Ce problème est indécidable en général pour les protocoles de sécurité. En pratique et pour des classes particulières de protocoles, des procédures de semi-décision existent mais nécessitent souvent une certaine expertise. L’apport majeur de cette thèse consiste en l’automatisation d’une technique fondée sur des approximations en réécriture et à sa mise à disposition à partir de langages de haut niveau (HLPSL et PROUVE). En représentant la connaissance initiale de l’intrus et la configuration initiale du réseau par un langage d’automate d’arbres et en utilisant d’un côté un système de réécriture, spécifiant le protocole ainsi que le pouvoir d’action d’un intrus, et d’un autre côté une fonction d’approximation symbolique, une surestimation ou une sous-estimation de la connaissance réelle de l’intrus peut être calculée afin de respectivement démontrer qu’un protocole est sûr, ou qu’un protocole est non sûr, et ce pour un nombre non borné d’exécutions du protocole étudié et pour des propriétés de secret. Le tout est implanté dans l’outil automatique TA4SP. Pour préciser pourquoi un protocole est non sûr, une technique de reconstruction de traces dans un contexte d’approximations en réécriture a été élaborée. A l’aide d’une reconstruction ”en arrière” utilisant une nouvelle notion d’unification, un semi-algorithme construisant une trace de réécriture jusqu’à un terme de l’automate initial a été établi, ce qui permet d’exhiber des contre-exemples dans le domaine de la vérification.