Symbolic protocol analysis with disequality constraints modulo equational theories

Santiago Escobar, Catherine Meadows, Jose 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

Fingerprint

Equational Theory
Algebra
Modulo
Cryptographic Protocols
Formal Analysis
Equality Constraints
Soundness
Reachability
Unification
Search Space
Completeness
Equality
Reasoning
Paradigm
Demonstrate
Strategy

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

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

Symbolic protocol analysis with disequality constraints modulo equational theories. / Escobar, Santiago; Meadows, Catherine; Meseguer, Jose; Santiago, Sonia.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer-Verlag, 2015. p. 238-261 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9465).

Research output: Chapter in Book/Report/Conference proceedingChapter

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). Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9465, Springer-Verlag, pp. 238-261. https://doi.org/10.1007/978-3-319-25527-9_16
Escobar S, Meadows C, Meseguer J, Santiago S. 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). Springer-Verlag. 2015. p. 238-261. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-319-25527-9_16
Escobar, Santiago ; Meadows, Catherine ; Meseguer, Jose ; Santiago, Sonia. / Symbolic protocol analysis with disequality constraints modulo equational theories. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer-Verlag, 2015. pp. 238-261 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inbook{1a019d1acd02460d99e0add2174c4741,
title = "Symbolic protocol analysis with disequality constraints modulo equational theories",
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.",
author = "Santiago Escobar and Catherine Meadows and Jose Meseguer and Sonia Santiago",
year = "2015",
month = "1",
day = "1",
doi = "10.1007/978-3-319-25527-9_16",
language = "English (US)",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer-Verlag",
pages = "238--261",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

TY - CHAP

T1 - Symbolic protocol analysis with disequality constraints modulo equational theories

AU - Escobar, Santiago

AU - Meadows, Catherine

AU - Meseguer, Jose

AU - Santiago, Sonia

PY - 2015/1/1

Y1 - 2015/1/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84943633009&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84943633009&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-25527-9_16

DO - 10.1007/978-3-319-25527-9_16

M3 - Chapter

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 238

EP - 261

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

PB - Springer-Verlag

ER -