Biblio
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.
The Maude-NRL Protocol Analyzer (Maude-NPA) is a tool for reasoning about the security of cryptographic protocols in which the cryptosystems satisfy different equational properties. It tries to find secrecy or authentication attacks by searching backwards from an insecure attack state pattern that may contain logical variables, in such a way that logical variables become properly instantiated in order to find an initial state. The execution mechanism for this logical reachability is narrowing modulo an equational theory. Although Maude-NPA also possesses a forwards semantics naturally derivable from the backwards semantics, it is not suitable for state space exploration or protocol simulation.
In this paper we define an executable forwards semantics for Maude-NPA, instead of its usual backwards one, and restrict it to the case of concrete states, that is, to terms without logical variables. This case corresponds to standard rewriting modulo an equational theory. We prove soundness and completeness of the backwards narrowing-based semantics with respect to the rewriting-based forwards semantics. We show its effectiveness as an analysis method that complements the backwards analysis with new prototyping, simulation, and explicit-state model checking features by providing some experimental results.
We present a new paradigm for unification arising out of a technique commonly used in cryptographic protocol analysis tools that employ unification modulo equational theories. This paradigm relies on: (i) a decomposition of an equational theory into (R, E) where R is confluent, terminating, and coherent modulo E, and (ii) on reducing unifi- cation problems to a set of problems s =? t under the constraint that t remains R/E-irreducible. We call this method asymmetric unification . We first present a general-purpose generic asymmetric unification algorithm.and then outline an approach for converting special-purpose conventional unification algorithms to asymmetric ones, demonstrating it for exclusive-or with uninterpreted function symbols. We demonstrate how asymmetric unification can improve performanceby running the algorithm on a set of benchmark problems. We also give results on the complexity and decidability of asymmetric unification.
Protocols do not work alone, but together, one protocol relying on another to provide needed services. Many of the problems in cryptographic protocols arise when such composition is done incorrectly or is not well understood. In this paper we discuss an extension to the Maude-NPA syntax and operational semantics to support dynamic sequential composition of protocols, so that protocols can be specified sepa- rately and composed when desired. This allows one to reason about many different compositions with minimal changes to the specification. Moreover, we show that, by a simple protocol transformation, we are able to analyze and verify this dynamic composition in the current Maude-NPA tool. We prove soundness and completeness of the protocol transforma- tion with respect to the extended operational semantics, and illustrate our results on some examples.