TY - GEN
T1 - Protocol analysis modulo combination of theories
T2 - 6th International ERCIM Workshop on Security and Trust Management, STM 2010
AU - Sasse, Ralf
AU - Escobar, Santiago
AU - Meadows, Catherine
AU - Meseguer, José
N1 - Funding Information:
R. Sasse and J. Meseguer have been partially supported by NSF Grants CNS-0716638, CNS-0831064 and CNS-0904749. S. Escobar has been partially supported by the EU (FEDER) and the Spanish MEC/MICINN under grant TIN 2007-68093-C02-02. C. Meadows has been partially supported by NSF Grant CNS-0904749.
PY - 2011
Y1 - 2011
N2 - There is a growing interest in formal methods and tools to analyze cryptographic protocols modulo algebraic properties of their underlying cryptographic functions. It is well-known that an intruder who uses algebraic equivalences of such functions can mount attacks that would be impossible if the cryptographic functions did not satisfy such equivalences. In practice, however, protocols use a collection of well-known functions, whose algebraic properties can naturally be grouped together as a union of theories E 1... ∪ n. Reasoning symbolically modulo the algebraic properties E1... ∪ n requires performing (E 1... ∪ n)-unification. However, even if a unification algorithm for each individual Ei is available, this requires combining the existing algorithms by methods that are highly non-deterministic and have high computational cost. In this work we present an alternative method to obtain unification algorithms for combined theories based on variant narrowing. Although variant narrowing is less efficient at the level of a single theory Ei, it does not use any costly combination method. Furthermore, it does not require that each Ei has a dedicated unification algorithm in a tool implementation. We illustrate the use of this method in the Maude-NPA tool by means of a well-known protocol requiring the combination of three distinct equational theories.
AB - There is a growing interest in formal methods and tools to analyze cryptographic protocols modulo algebraic properties of their underlying cryptographic functions. It is well-known that an intruder who uses algebraic equivalences of such functions can mount attacks that would be impossible if the cryptographic functions did not satisfy such equivalences. In practice, however, protocols use a collection of well-known functions, whose algebraic properties can naturally be grouped together as a union of theories E 1... ∪ n. Reasoning symbolically modulo the algebraic properties E1... ∪ n requires performing (E 1... ∪ n)-unification. However, even if a unification algorithm for each individual Ei is available, this requires combining the existing algorithms by methods that are highly non-deterministic and have high computational cost. In this work we present an alternative method to obtain unification algorithms for combined theories based on variant narrowing. Although variant narrowing is less efficient at the level of a single theory Ei, it does not use any costly combination method. Furthermore, it does not require that each Ei has a dedicated unification algorithm in a tool implementation. We illustrate the use of this method in the Maude-NPA tool by means of a well-known protocol requiring the combination of three distinct equational theories.
KW - Cryptographic protocol verification
KW - equational unification
KW - exclusive or
KW - narrowing
KW - variants
UR - http://www.scopus.com/inward/record.url?scp=80054053953&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=80054053953&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-22444-7_11
DO - 10.1007/978-3-642-22444-7_11
M3 - Conference contribution
AN - SCOPUS:80054053953
SN - 9783642224430
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 163
EP - 178
BT - Security and Trust Management - 6th International Workshop, STM 2010, Revised Selected Papers
Y2 - 23 September 2010 through 24 September 2010
ER -