Notions of Knowledge in Combinations of Theories Sharing Constructors

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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [26 references]  Display  Hide  Download

https://hal.inria.fr/hal-01587181
Contributor : Christophe Ringeissen <>
Submitted on : Wednesday, September 13, 2017 - 5:43:20 PM
Last modification on : Thursday, February 7, 2019 - 2:59:47 PM
Long-term archiving on : Thursday, December 14, 2017 - 2:03:06 PM

File

combi-know.pdf
Files produced by the author(s)

Identifiers

Citation

Serdar Erbatur, Andrew Marshall, Christophe Ringeissen. Notions of Knowledge in Combinations of Theories Sharing Constructors. 26th International Conference on Automated Deduction, Aug 2017, Göteborg, Sweden. pp.60 - 76, ⟨10.1007/978-3-319-63046-5_5⟩. ⟨hal-01587181⟩

Share

Metrics

Record views

294

Files downloads

107