TY - GEN
T1 - A rewriting-based forwards semantics for Maude-NPA
AU - Escobar, Santiago
AU - Meadows, Catherine
AU - Meseguer, José
AU - Santiago, Sonia
PY - 2014
Y1 - 2014
N2 - 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 reach-ability 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.
AB - 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 reach-ability 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.
KW - Cryptographic protocol analysis
KW - Logical narrowing-based reachability analysis
KW - Reasoning modulo an equational theory
KW - Standard rewriting-based model checking
UR - http://www.scopus.com/inward/record.url?scp=84906813742&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84906813742&partnerID=8YFLogxK
U2 - 10.1145/2600176.2600186
DO - 10.1145/2600176.2600186
M3 - Conference contribution
AN - SCOPUS:84906813742
SN - 9781450329071
T3 - ACM International Conference Proceeding Series
BT - Proceedings of the 2014 Symposium and Bootcamp on the Science of Security, HotSoS 2014
PB - Association for Computing Machinery
T2 - 2014 Symposium and Bootcamp on the Science of Security, HotSoS 2014
Y2 - 8 April 2014 through 9 April 2014
ER -