Cheval, Vincent, Cortier, Véronique, Delaune, Stéphanie (2013) Deciding equivalencebased properties using constraint solving. Theoretical Computer Science, 492 . pp. 139. ISSN 03043975. (doi:10.1016/j.tcs.2013.04.016)
PDF  Publisher pdf  
Download (590kB)
Preview



Official URL http://dx.doi.org/10.1016/j.tcs.2013.04.016 
Abstract
Formal methods have proved their usefulness for analyzing the security of protocols. Most existing results focus on trace properties like secrecy or authentication. There are however several security properties, which cannot be defined (or cannot be naturally defined) as trace properties and require a notion of behavioural equivalence. Typical examples are anonymity, privacy related properties or statements closer to security properties used in cryptography. In this paper, we consider three notions of equivalence defined in the applied pi calculus: observational equivalence, maytesting equivalence, and trace equivalence. First, we study the relationship between these three notions. We show that for determinate processes, observational equivalence actually coincides with trace equivalence, a notion simpler to reason with. We exhibit a large class of determinate processes, called simple processes, that capture most existing protocols and cryptographic primitives. While trace equivalence and maytesting equivalence seem very similar, we show that maytesting equivalence is actually strictly stronger than trace equivalence. We prove that the two notions coincide for imagefinite processes, such as processes without replication. Second, we reduce the decidability of trace equivalence (for finite processes) to deciding symbolic equivalence between sets of constraint systems. For simple processes without replication and with trivial else branches, it turns out that it is actually sufficient to decide symbolic equivalence between pairs of positive constraint systems. Thanks to this reduction and relying on a result first proved by M. Baudet, this yields the first decidability result of observational equivalence for a general class of equational theories (for processes without else branch nor replication). Moreover, based on another decidability result for deciding equivalence between sets of constraint systems, we get decidability of trace equivalence for processes with else branch for standard primitives.
Item Type:  Article 

DOI/Identification number:  10.1016/j.tcs.2013.04.016 
Subjects: 
Q Science > QA Mathematics (inc Computing science) > QA 75 Electronic computers. Computer science Q Science > QA Mathematics (inc Computing science) > QA 9 Formal systems, logics 
Divisions:  Faculties > Sciences > School of Computing > Security Group 
Depositing User:  Vincent Cheval 
Date Deposited:  23 Jan 2015 11:29 UTC 
Last Modified:  29 May 2019 14:05 UTC 
Resource URI:  https://kar.kent.ac.uk/id/eprint/46725 (The current URI for this page, for reference purposes) 
 Export to:
 RefWorks
 EPrints3 XML
 BibTeX
 CSV
 Depositors only (login required):