TY - JOUR
T1 - A formal definition of protocol indistinguishability and its verification using maude-NPA
AU - Santiago, Sonia
AU - Escobar, Santiago
AU - Meadows, Catherine
AU - Meseguer, José
N1 - Funding Information:
Santiago Escobar and Sonia Santiago have been partially supported by the EU (FEDER) and the Spanish MINECO under grants TIN 2010-21062-C02-02 and TIN 2013-45732-C4-1-P, and by Generalitat Valenciana PROMETEO2011/052. José Meseguer has been partially supported by NSF Grant CNS 13-10109.
Publisher Copyright:
© Springer International Publishing Switzerland 2014.
PY - 2014
Y1 - 2014
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84921723088&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84921723088&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-11851-2_11
DO - 10.1007/978-3-319-11851-2_11
M3 - Article
AN - SCOPUS:84921723088
VL - 8743
SP - 162
EP - 177
JO - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
JF - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SN - 0302-9743
ER -