Protocol analysis modulo combination of theories: A case study in maude-NPA

Ralf Sasse, Santiago Escobar, Catherine Meadows, José Meseguer

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.

Original languageEnglish (US)
Title of host publicationSecurity and Trust Management - 6th International Workshop, STM 2010, Revised Selected Papers
Number of pages16
StatePublished - 2011
Event6th International ERCIM Workshop on Security and Trust Management, STM 2010 - Athens, Greece
Duration: Sep 23 2010Sep 24 2010

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6710 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other6th International ERCIM Workshop on Security and Trust Management, STM 2010


  • Cryptographic protocol verification
  • equational unification
  • exclusive or
  • narrowing
  • variants

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Protocol analysis modulo combination of theories: A case study in maude-NPA'. Together they form a unique fingerprint.

Cite this