TY - GEN
T1 - Effective symbolic protocol analysis via equational irreducibility conditions
AU - Erbatur, Serdar
AU - Escobar, Santiago
AU - Kapur, Deepak
AU - Liu, Zhiqiang
AU - Lynch, Christopher
AU - Meadows, Catherine
AU - Meseguer, José
AU - Narendran, Paliath
AU - Santiago, Sonia
AU - Sasse, Ralf
N1 - S. Escobar and S. Santiago have been partially supported by the EU (FEDER) and the Spanish MEC/MICINN under grant TIN 2010-21062-C02-02, and by Generalitat Valenciana PROMETEO2011/052. The following authors have been partially supported by NSF: S. Escobar, J. Meseguer and R. Sasse under grants CCF 09-05584, CNS 09-04749, and CNS 09-05584; D. Kapur under grant CNS 09-05222; C. Lynch, Z. Liu, and C. Meadows under grant CNS 09-05378, and P. Narendran and S. Erbatur under grant CNS 09-05286.
PY - 2012
Y1 - 2012
N2 - We address a problem that arises in cryptographic protocol analysis when the equational properties of the cryptosystem are taken into account: in many situations it is necessary to guarantee that certain terms generated during a state exploration are in normal form with respect to the equational theory. We give a tool-independent methodology for state exploration, based on unification and narrowing, that generates states that obey these irreducibility constraints, called contextual symbolic reachability analysis, prove its soundness and completeness, and describe its implementation in the Maude-NPA protocol analysis tool. Contextual symbolic reachability analysis also introduces a new type of unification mechanism, which we call asymmetric unification, in which any solution must leave the right side of the solution irreducible. We also present experiments showing the effectiveness of our methodology.
AB - We address a problem that arises in cryptographic protocol analysis when the equational properties of the cryptosystem are taken into account: in many situations it is necessary to guarantee that certain terms generated during a state exploration are in normal form with respect to the equational theory. We give a tool-independent methodology for state exploration, based on unification and narrowing, that generates states that obey these irreducibility constraints, called contextual symbolic reachability analysis, prove its soundness and completeness, and describe its implementation in the Maude-NPA protocol analysis tool. Contextual symbolic reachability analysis also introduces a new type of unification mechanism, which we call asymmetric unification, in which any solution must leave the right side of the solution irreducible. We also present experiments showing the effectiveness of our methodology.
UR - https://www.scopus.com/pages/publications/84865601872
UR - https://www.scopus.com/pages/publications/84865601872#tab=citedBy
U2 - 10.1007/978-3-642-33167-1_5
DO - 10.1007/978-3-642-33167-1_5
M3 - Conference contribution
AN - SCOPUS:84865601872
SN - 9783642331664
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 73
EP - 90
BT - Computer Security, ESORICS 2012 - 17th European Symposium on Research in Computer Security, Proceedings
T2 - 17th European Symposium on Research in Computer Security, ESORICS 2012
Y2 - 10 September 2012 through 12 September 2012
ER -