SPOOC: Notions of Knowledge in Combinations of Theories Sharing Constructors

Notions of Knowledge in Combinations of Theories Sharing Constructors

Serdar Erbatur, Andrew M. Marshall, and Christophe Ringeissen. Notions of Knowledge in Combinations of Theories Sharing Constructors. In Proceedings of 26th International Conference on Automated Deduction (CADE'17), Lecture Notes in Computer Science, Springer, Gothenburg, Sweden, August 2017.
doi:10.1007/978-3-319-63046-5

Download

[HTML]

Abstract

One of the most effective methods developed for the analysis of security protocols is an approach based on equational reasoning and unification. In this approach, it is important to have the capability to reason about the knowledge of an intruder. Two important measures of this knowledge, defined modulo equational theories, are deducibility and static equivalence. We present new combination techniques for the study of deducibility and static equivalence in unions of equational theories sharing constructors. Thanks to these techniques, we obtain new modularity results for the decidability of deducibility and static equivalence. In turn, this should allow for the analysis of protocols involving combined equational theories which previous disjoint combination methods could not address due to their non-disjoint axiomatization.

BibTeX

@inproceedings{EMR-cade17,
  abstract =	 {One of the most effective methods developed for the
                  analysis of security protocols is an approach based
                  on equational reasoning and unification. In this
                  approach, it is important to have the capability to
                  reason about the knowledge of an intruder. Two
                  important measures of this knowledge, defined modulo
                  equational theories, are deducibility and static
                  equivalence. We present new combination techniques
                  for the study of deducibility and static equivalence
                  in unions of equational theories sharing
                  constructors.  Thanks to these techniques, we obtain
                  new modularity results for the decidability of
                  deducibility and static equivalence. In turn, this
                  should allow for the analysis of protocols involving
                  combined equational theories which previous disjoint
                  combination methods could not address due to their
                  non-disjoint axiomatization.},
  address =	 {Gothenburg, Sweden},
  author =	 {Serdar Erbatur and Andrew M. Marshall and Christophe
                  Ringeissen},
  booktitle =	 {{P}roceedings of 26th International Conference on
                  Automated Deduction ({CADE}'17)},
  month =	 aug,
  publisher =	 {Springer},
  series =	 {Lecture Notes in Computer Science},
  title =	 {Notions of Knowledge in Combinations of Theories
                  Sharing Constructors},
  year =	 2017,
  acronym =	 {{CADE}'17},
  nmonth =	 8,
  url =		 {https://doi.org/10.1007/978-3-319-63046-5},
  doi =		 {10.1007/978-3-319-63046-5},
}