Symbolic protocol analysis with disequality constraints modulo equational theories

Santiago Escobar, Catherine Meadows, José Meseguer, Sonia Santiago

Research output: Chapter in Book/Report/Conference proceedingChapter

Abstract

Research in the formal analysis of cryptographic protocols has produced much good work in the solving of equality constraints, developing new methods for unification, matching, and deducibility. However, considerably less attention has been paid to disequality constraints. These also arise quite naturally in cryptographic protocol analysis, in particular for analysis of indistinguishability properties. Thus methods for deciding whether or not they are satisfiable could potentially be quite useful in reducing the size of the search space by protocol analysis tools. In this paper we develop a framework for reasoning about disequality constraints centered around the paradigm of the most discriminating Dolev-Yao attacker, who is able to detect a disequality if it is satisfied in some implementation of the crypto-algebra satisfying given equality properties. We develop several strategies for handling disequalities, prove their soundness and completeness, and demonstrate the result of experimental analyses using the various strategies. Finally, we discuss how disequality checking algorithms could be incorporated within symbolic reachability protocol analysis methods.

Original languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PublisherSpringer-Verlag
Pages238-261
Number of pages24
DOIs
StatePublished - Jan 1 2015

Publication series

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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Symbolic protocol analysis with disequality constraints modulo equational theories'. Together they form a unique fingerprint.

  • Cite this

    Escobar, S., Meadows, C., Meseguer, J., & Santiago, S. (2015). Symbolic protocol analysis with disequality constraints modulo equational theories. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 238-261). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9465). Springer-Verlag. https://doi.org/10.1007/978-3-319-25527-9_16