Foundations and Analysis of Protocol Indistinguishability

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 ).