Résumé | Secure design of communication protocols in order to ensure the authen- tication of electronic agents or the safety of secret data is known to be difficult and fairly error-prone. Symbolic frameworks such as the Dolev-Yao model and later various process algebra have proven themselves valuable for finding attacks and assessing the security of these protocols. Several tools have thus been developed to answer the need of automated verification: ProVerif, AVISPA and Scyther rely on various formal methods to prove that a range of security properties holds in protocols.
The problem of deciding reachability for cryptographic protocols has been thoroughly studied for an unbounded number of sessions and proven to be undecidable in general. Nevertheless some fragments were shown to be decidable, either by tagging or by restricting the number of blind-copies. On the other hand, trace equivalence has only been proven to be decidable for a bounded number of sessions. The objective of this talk is to provide the first results of decidability of trace equivalence for an unbounded number of sessions.
Trace equivalence for a first class of protocols was shown undecidable under scarce restrictions one variable and symmetric encryption are indeed enough. Consequently, we restrained our class of protocols a step further by making the protocols deterministic in some sense and preventing it from disclosing secret keys. This tighter class of protocols was then shown to be decidable after reduction to an equivalence between deterministic pushdown automata. |