Résumé
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.
Source: http://www.theses.fr/2006BESA2042
.
