Maude-NPA: Equation-Aware Cryptographic Protocal Analysis
Abstract:
One area that has been particularly productive in the rapidly growing field of formal analysis of cryptographic protocols is development of special-purpose model checkers. These tools use variants of the Dolev-Yao model to search through different concurrent executions of a protocol in the face of a network controlled by an attacker who can read, alter, and redirect traffic using operations available to an honest principal. These tools have been extremely effective at finding non-intuitive flaws in protocol design.
However, it has increasingly been realized that there is a need not to only be able to list the operations that are used in the protocol but to specify and reason about the algebraic properties as well. This is because many cryptographic algorithms and protocols depend on these algebraic properties as well. This is because many cryptographic algorithms and protocols depend on these algebraic properties to achieve their goals. Probably the best-known example is Diffie-Hellman key exchange, which uses an exponentiation operator exp such that exp(exp(x, a), b) = exp(x, a*b) where * is associative-commutative. Moreover, these very algebraic properties can also be used by attackers to defeat the protocols.
These algebraic properties can be easily expressed as equations involving the operators used in the protocol. However, incorporating the equations within protocol analysis is not trivial. In order to be effective a tool must be capable of reasoning about protocols that use, not only a particular equational theory, but different combinations of equational theories. This is especially the case when protocols that use different algorithms are composed, as is often the case.
The Maude-NRL Protocol Analyzer (Maude-NPA for short), is a tool that was designed specifically for reasoning about protocols that rely on different combinations of equational theories. It produces symbolic traces, that is traces that may contain logical variables Although the general problem of deciding security in the Dolve-Yao model is undecidable when an unbounded number of protocol executions is allowed, Maude-NPA is often able to decide security in these cases by a combination its symbolic approach and inductive state-space reduction techniques. Maude-NPA determines security by searching backwards to an initial state specified by the user, producing an attack trace if it is successful.
Maude-NPS’s backwards search algorithm is based on unification and narrowing modulo an equational theory E, where E is the theory describing the behavior of the operations used in the protocol. Unification solves the problem of determining which substitutions to the variables in two states make the two states the same modulo E. Narrowing allows us to unify the output of a state transition with a substate of a symbolic to determine what symbolic state must precede it. We have developed a general unification algorithm, folding variant narrowing, that applies to the case in which he equational theory E is a composition of theories (R, ∆), in which R is a set of rewrite rules, that is, rules that can be given an orientation l → r, and the other is a commonly occurring theory such as the associative commutative theory (AC). The other requirements on R with respect to ∆ are either easily checkable or have been thoroughly studied in the literature, with automated support available. When one wishes to compose two theories (R1, ∆) and (R2, ∆), all that is required is to check whether the R1 and R2 satisfy these properties. Combining two theories ∆1 and ∆2 is harder, but the underlying Maude engine supports such combinations for commonly occurring sets of axioms.
In this poster we will give an overview of the Maude-NPA tool and how it applies folding variant narrowing to support composition of theories and protocols. We will also demonstrate the use of Maude-NPA and discuss future plans. The Maude-NPA tool is available for download at http://maude.cs.uiuc.edu/tools/Maude-NPA/.
Biography:
Dr. Meadows is a senior researcher in computer security at the Center for High Assurance Systems at the Naval Research Laboratory (NRL), heading that group’s Formal Methods Section. She was the principle developer of the NRL Protocol Analyzer (NPA), which was one of the first software tools to find previously undiscovered flaws in cryptographic protocols, and has been used successfully in analysis of a large number of protocols, including the Internet Key Exchange Protocol and the Group Domain of Interpretation protocol, both of which because standards for the Internet Engineering Task Force. Currently she is co-PI on a project that is developing a successor to the NRL Protocol Analyzer, Maude-NPA, which allows more fine-grained specification of crypto-algorithms than NPA. Other projects she is involved with include the machine-verified analysis of crypto-algorithms and protocols for the IARPA-sponsored Security and Privacy Assurance Research Program, and the development of logical systems for reasoning about the security of protocols for pervasive computing. Prior to joining NRL, she was on the mathematics faculty at Texas A&M University. There she worked in various areas of cryptography, including secret sharing schemes and software protection. She received her Ph.D. in mathematics from the University of Illinois at Urbana-Champaign.