2011 | OriginalPaper | Buchkapitel
Protocol Analysis Modulo Combination of Theories: A Case Study in Maude-NPA
verfasst von : Ralf Sasse, Santiago Escobar, Catherine Meadows, José Meseguer
Erschienen in: Security and Trust Management
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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
∪ … ∪
E
n
. Reasoning symbolically modulo the algebraic properties
E
1
∪ … ∪
E
n
requires performing (
E
1
∪ … ∪
E
n
)-unification. However, even if a unification algorithm for each individual
E
i
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
E
i
, it does not use any costly combination method. Furthermore, it does not require that each
E
i
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.