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 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.
|Original language||English (US)|
|Number of pages||16|
|Journal||Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|
|State||Published - 2014|
ASJC Scopus subject areas
- Theoretical Computer Science
- Computer Science(all)