On the decidability of reachability problems for cryptographic protocols
Mounira Kourjieh :: Thursday 6th November 2008
Venue: Room 124 @ 1130 (Unusual time/place)
Abstract. In the symbolic analysis of cryptographic protocols, we represent the knowledge of agents by terms and the behaviour of the intruder by deduction rules. These terms may employ cryptographic functions (hash functions, public encryption, symmetric encryption, digital signature, blind signature, etc.) and these functions may have algebraic properties. These properties are represented by equational theories. In this presentation, we will focus on cryptographic protocols that use function symbols represented by convergent equational theories having finite variant property. We present a saturation algorithm for the set of intruder deduction rules, we show that the termination of this saturation entails the decidability of the ground reachability problem, i.e. in the case of passive intruder. We show also that it is necessary to add one other condition to obtain the decidability of non-ground reachability problem, i.e. in the case of active intruder, and provide one new such criterion.