Effective symbolic protocol analysis via equational irreducibility conditions

Serdar Erbatur, Santiago Escobar, Deepak Kapur, Zhiqiang Liu, Christopher Lynch, Catherine Meadows, José Meseguer, Paliath Narendran, Sonia Santiago, Ralf Sasse

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publicationComputer Security, ESORICS 2012 - 17th European Symposium on Research in Computer Security, Proceedings
Pages73-90
Number of pages18
DOIs
StatePublished - 2012
Event17th European Symposium on Research in Computer Security, ESORICS 2012 - Pisa, Italy
Duration: Sep 10 2012Sep 12 2012

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7459 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other17th European Symposium on Research in Computer Security, ESORICS 2012
CountryItaly
CityPisa
Period9/10/129/12/12

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Effective symbolic protocol analysis via equational irreducibility conditions'. Together they form a unique fingerprint.

Cite this