A Proof Theoretic Analysis of Intruder Theories

Altmetric Citations
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 naturaldeductionlike systems and proving decidability requires significant effort in showing that the rules...[Show more]
dc.contributor.author  Tiu, Alwen  

dc.contributor.author  Gore, Rajeev  
dc.coverage.spatial  Brazil  
dc.date.accessioned  20151207T22:17:42Z  
dc.date.created  June 29July 1 2009  
dc.identifier.isbn  3642023479  
dc.identifier.uri  http://hdl.handle.net/1885/18702  
dc.description.abstract  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 naturaldeductionlike systems and proving decidability requires significant effort in showing that the rules are "local" in some sense. By using the wellknown 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 ACconvergent 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.publisher  Springer  
dc.relation.ispartofseries  International conference on Rewriting Techniques and Applications (RTA 2009)  
dc.source  RTA 2009: Proceedings of the International Conference on Rewriting Techniques & Applications  
dc.source.uri  http://www.springerlink.com  
dc.subject  Keywords: AC convergent theories; Associativity; Binary operators; Blind signatures; Commutativity; Cut elimination; Equational theory; Intruder deduction; Natural deduction; Polynomialtime; Proof search; Prooftheoretic method; Security protocol analysis; Securit AC convergent theories; Intruder deduction; Security protocols; Sequent calculus  
dc.title  A Proof Theoretic Analysis of Intruder Theories  
dc.type  Conference paper  
local.description.notes  Imported from ARIES  
local.description.refereed  Yes  
dc.date.issued  2009  
local.identifier.absfor  080203  Computational Logic and Formal Languages  
local.identifier.absfor  010107  Mathematical Logic, Set Theory, Lattices and Universal Algebra  
local.identifier.ariespublication  u4607519xPUB5  
local.type.status  Published Version  
local.contributor.affiliation  Tiu, Alwen, College of Engineering and Computer Science, ANU  
local.contributor.affiliation  Gore, Rajeev, College of Engineering and Computer Science, ANU  
local.description.embargo  20371231  
local.bibliographicCitation.startpage  103  
local.bibliographicCitation.lastpage  117  
local.identifier.doi  10.1007/9783642023484_8  
dc.date.updated  20160224T11:13:55Z  
local.identifier.scopusID  2s2.070350677091  
Collections  ANU Research Publications 
Download
File  Description  Size  Format  Image 

01_Tiu_A_Proof_Theoretic_Analysis_of_2009.pdf  377.62 kB  Adobe PDF  Request a copy  
02_Tiu_A_Proof_Theoretic_Analysis_of_2009.pdf  95.16 kB  Adobe PDF  Request a copy  
03_Tiu_A_Proof_Theoretic_Analysis_of_2009.pdf  525.98 kB  Adobe 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