Complexity of automatic verification of cryptographic protocols
Many security properties are naturally expressed in terms of indistinguishability.
In symbolic protocol models the notion of indistinguishability can be expressed as trace equivalence in a cryptographic process calculus. Current automated verification tools are however limited even for a bounded number of sessions: they are either restricted to support only a particular set of cryptographic primitives, do not allow for protocols with else branches, or can only approximate trace equivalence, allowing for false attacks. Moreover, the complexity of these algorithms has never been studied.
In this work, we study the complexity of deciding equivalence properties, for several classes of protocols and several equivalences.
Thème(s) : Conférences Recherche