A Formal Definition of Protocol Indistinguishability and its Verification Using Maude-NPA

Intuitively, two protocols P₁ and P₂ are indistinguishable if an attacker cannot tell the difference between interactions with P₁ and with P₂ . In this paper we: (i) propose an intuitive notion of indistinguishability in Maude-NPA; (ii) formalize such a notion in terms of state unreachability conditions on their synchronous product; (iii) prove theorems showing how --assuming the protocol's algebraic theory has a finite variant (FV) decomposition - these conditions can be checked by the Maude-NPA tool; and (iv) illustrate our approach with concrete examples. This provides for the first time a framework for automatic analysis of indistinguishability modulo as wide a class of algebraic properties as FV, which includes many associative-commutative theories of interest to cryptographic protocol analysis.