Skip navigation
Skip navigation

A Proof Theoretic Analysis of Intruder Theories

Tiu, Alwen; Gore, Rajeev

Description

We consider the problem of intruder deduction in security protocol analysis: that is, deciding whether a given message M can be deduced from a set of messages F under the theory of blind signatures and arbitrary convergent equational theories modulo associativity and commutativity (AC) of certain binary operators. The traditional formulations of intruder deduction are usually given in natural-deduction-like systems and proving decidability requires significant effort in showing that the rules...[Show more]

dc.contributor.authorTiu, Alwen
dc.contributor.authorGore, Rajeev
dc.coverage.spatialBrazil
dc.date.accessioned2015-12-07T22:17:42Z
dc.date.createdJune 29-July 1 2009
dc.identifier.isbn3642023479
dc.identifier.urihttp://hdl.handle.net/1885/18702
dc.description.abstractWe consider the problem of intruder deduction in security protocol analysis: that is, deciding whether a given message M can be deduced from a set of messages F under the theory of blind signatures and arbitrary convergent equational theories modulo associativity and commutativity (AC) of certain binary operators. The traditional formulations of intruder deduction are usually given in natural-deduction-like systems and proving decidability requires significant effort in showing that the rules are "local" in some sense. By using the well-known translation between natural deduction and sequent calculus, we recast the intruder deduction problem as proof search in sequent calculus, in which locality is immediate. Using standard proof theoretic methods, such as permutability of rules and cut elimination, we show that the intruder deduction problem can be reduced, in polynomial time, to the elementary deduction problems, which amounts to solving certain equations in the underlying individual equational theories. We further show that this result extends to combinations of disjoint AC-convergent theories whereby the decidability of intruder deduction under the combined theory reduces to the decidability of elementary deduction in each constituent theory. Although various researchers have reported similar results for individual cases, our work shows that these results can be obtained using a systematic and uniform methodology based on the sequent calculus.
dc.publisherSpringer
dc.relation.ispartofseriesInternational conference on Rewriting Techniques and Applications (RTA 2009)
dc.sourceRTA 2009: Proceedings of the International Conference on Rewriting Techniques & Applications
dc.source.urihttp://www.springerlink.com
dc.subjectKeywords: AC convergent theories; Associativity; Binary operators; Blind signatures; Commutativity; Cut elimination; Equational theory; Intruder deduction; Natural deduction; Polynomial-time; Proof search; Proof-theoretic method; Security protocol analysis; Securit AC convergent theories; Intruder deduction; Security protocols; Sequent calculus
dc.titleA Proof Theoretic Analysis of Intruder Theories
dc.typeConference paper
local.description.notesImported from ARIES
local.description.refereedYes
dc.date.issued2009
local.identifier.absfor080203 - Computational Logic and Formal Languages
local.identifier.absfor010107 - Mathematical Logic, Set Theory, Lattices and Universal Algebra
local.identifier.ariespublicationu4607519xPUB5
local.type.statusPublished Version
local.contributor.affiliationTiu, Alwen, College of Engineering and Computer Science, ANU
local.contributor.affiliationGore, Rajeev, College of Engineering and Computer Science, ANU
local.description.embargo2037-12-31
local.bibliographicCitation.startpage103
local.bibliographicCitation.lastpage117
local.identifier.doi10.1007/978-3-642-02348-4_8
dc.date.updated2016-02-24T11:13:55Z
local.identifier.scopusID2-s2.0-70350677091
CollectionsANU Research Publications

Download

File Description SizeFormat Image
01_Tiu_A_Proof_Theoretic_Analysis_of_2009.pdf377.62 kBAdobe PDF    Request a copy
02_Tiu_A_Proof_Theoretic_Analysis_of_2009.pdf95.16 kBAdobe PDF    Request a copy
03_Tiu_A_Proof_Theoretic_Analysis_of_2009.pdf525.98 kBAdobe PDF    Request a copy


Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator