ABSTRACT
Intuitively, two protocols P1 and P2 are indistinguishable if an attacker cannot tell the difference between interactions with P1 and with P2. In this paper we: (i) propose an intuitive notion of indistin- guishability that applies to protocols whose equational theories satisfy the finite variant (FV) property, a wide class of algebraic theories for cryptographic protocols; (ii) formalize such a notion in terms of what we call their synchronous product P1 P2 and of two simpler notions, the indistiguishable messages (IM ) property, and the indistiguishable at- tacker event sequences (IAES) property; (iii) prove theorems showing how the (IM ) and (IAES ) properties can be checked by the Maude-NPA tool; and (iv) illustrate such verification with concrete examples. To the best of our knowledge, this work makes possible for the first time the automatic verification of indistinguishability modulo as wide a class of algebraic properties as (FV ).
Switch to experimental viewer