TY - JOUR
T1 - Equational Cryptographic Reasoning in the Maude-NRL Protocol Analyzer
AU - Escobar, Santiago
AU - Meadows, Catherine
AU - Meseguer, José
N1 - Funding Information:
1 Email:[email protected] 2 Email:[email protected] 3 Email:[email protected] 4 S. Escobar has been partially supported by the EU (FEDER) and Spanish MEC TIN-2004-7943-C04-02 project, the Generalitat Valenciana under grant GV06/285, and the ICT for EU-India Cross-Cultural Dissemination ALA/95/23/2003/077-054 project.
PY - 2007/7/10
Y1 - 2007/7/10
N2 - 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.
AB - 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.
KW - Cryptographic Protocol Verification
KW - Equational Reasoning
KW - Maude
KW - Narrowing
KW - Rewriting Logic
UR - http://www.scopus.com/inward/record.url?scp=34250834342&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=34250834342&partnerID=8YFLogxK
U2 - 10.1016/j.entcs.2007.02.053
DO - 10.1016/j.entcs.2007.02.053
M3 - Article
AN - SCOPUS:34250834342
SN - 1571-0661
VL - 171
SP - 23
EP - 36
JO - Electronic Notes in Theoretical Computer Science
JF - Electronic Notes in Theoretical Computer Science
IS - 4
ER -