Name
Abstract | ||
|---|---|---|
The NRL Protocol Analyzer (NPA) is a tool for the formal specification and analysis of cryptographic protocols that has been used with great effect on a number of complex real-life protocols. One of the most interesting of its features is that it can be used to reason about security in face of attempted attacks on low-level algebraic properties of the functions used in a protocol. Recently, we have given for the first time a precise formal specification of the main features of the NPA inference system: its grammar-based techniques for (co-)invariant generation and its backwards narrowing reachability analysis method; both implemented in Maude as the Maude-NPA tool. This formal specification is given within the well-known rewriting framework so that the inference system is specified as a set of rewrite rules modulo an equational theory describing the behavior of the cryptographic symbols involved. This paper gives a high-level overview of the Maude-NPA tool and illustrates how it supports equational reasoning about properties of the underlying cryptographic infrastructure by means of a simple, yet nontrivial, example of an attack whose discovery essentially requires equational reasoning. It also shows how rule-based programming languages such as Maude and complex narrowing strategies are useful to model, analyze, and verify protocols. |
Year | DOI | Venue |
|---|---|---|
2007 | 10.1016/j.entcs.2007.02.053 | Electr. Notes Theor. Comput. Sci. |
Keywords | Field | DocType |
cryptographic symbol,equational reasoning,maude-nrl protocol analyzer,narrowing,npa inference system,backwards narrowing reachability analysis,rewriting logic,maude,cryptographic protocol,equational theory,precise formal specification,equational cryptographic reasoning,maude-npa tool,cryptographic protocol verification,formal specification,underlying cryptographic infrastructure | Packet analyzer,Programming language,Cryptographic protocol,Computer science,Modulo,Cryptography,Theoretical computer science,Formal specification,Reachability,Cryptographic primitive,Rewriting | Journal |
Volume | Issue | ISSN |
171 | 4 | Electronic Notes in Theoretical Computer Science |
Citations | PageRank | References |
16 | 0.84 | 17 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Santiago Escobar | 1 | 452 | 27.87 |
| Catherine Meadows | 2 | 928 | 89.05 |
| José Meseguer | 3 | 9533 | 805.39 |