Download as a PDF

The earliest protocol analysis tools, such as the Interrogator [30] and the NRL
Protocol Analyzer (NPA) [35], while not strictly speaking model checkers, relied
on state exploration, and, in the case of NPA, could be used to verify security
properties specied in a temporal logic language. Later, researchers used generic
model checkers to analyze protocols, such as FDR [32] and later Murphi [40].
More recently the focus has been on special-purpose model-checkers developed
specically for cryptographic protocol analysis, such as Blanchet's ProVerif [8],
the AVISPA tool [3], and Maude-NPA itself [23].
There are a number of possible approaches to take in the modeling of cryptoalgorithms used. In the simplest case, the free algebra model, cryptosystems
are assumed to behave like black boxes: an attacker knows nothing about encrypted data unless it has the appropriate key. This is the approach taken, for
example, by the above-cited use of Murphi and FDR to analyze cryptographic
protocols, and current tools such as SATMC [4] and TA4SP [9] , both used in the
AVISPA tool. However, such an approach, although it can work well for protocols based on generic shared key or public key cryptography, runs into problems
with algorithms such as Die-Hellman or algorithms employing exclusive-or,
which rely upon various algebraic properties such as the law of exponentiation
of products, associativity-commutativity and cancellation. Without the ability
to specify these properties, one needs to rely on approximations of the algorithms
that may result in formal proofs of secrecy invalidated by actual attacks that are
missed by the analysis (see, e.g., [41,43,46]). Thus there has been considerable
interest in developing algorithms and tools for protocol analysis in the presence
of algebraic theories [1,11,10,12,7].
Another way in which tools can dier is in the number of sessions. A session is
dened to be one execution of a protocol role by a single principal. A tool is said
to use the bounded session model if the user must specify the maximum number
of sessions that can be generated in a search. It is said to use the unbounded
session model if no such restrictions are required.
Secrecy is known to be decidable in the free theory together with the bounded
session model [42], and undecidable in the free theory together with the unbounded session model [18]. The same distinction between bounded and unbounded sessions is known to hold for a number of dierent equational theories
of interest, as well as for some authentication-related properties; see for example
[10]. Thus, it is no surprise that most tools, whether or not they oer support
for dierent algebraic theories, either operate in the bounded session model, or
rely on abstractions that may result in reports of false attacks even when the
protocol being analyzed is secure.
Maude-NPA is a model-checker for cryptographic protocol analysis that both
allows for the incorporation of dierent equational theories and operates in the
unbounded session model without the use of abstraction. This means that the
analysis is exact. That is, (i) if an attack exists using the specied algebraic
properties, it will be found; (ii) no false attacks will be reported; and (iii) if
the tool terminates without nding an attack, this provides a formal proof that
the protocol is secure for that attack modulo the specied properties. However,
2