Reduction of Equational Theories for Verification of Trace Equivalence: Re-encryption, Associativity and Commutativity

Myrto Arapinis, Sergiu Bursuc, MarkD. Ryan

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

Verification of trace equivalence is difficult to automate in general because it requires relating two infinite sets of traces. The problem becomes even more complex when algebraic properties of cryptographic primitives are taken in account in the formal model. For example, no verification tool or technique can currently handle automatically a realistic model of re-encryption or associative-commutative operators.
In this setting, we propose a general technique for reducing the set of traces that have to be analyzed to a set of local traces. A local trace restricts the way in which some function symbols are used, and this allows us to perform a second reduction, by showing that some algebraic properties can be safely ignored in local traces.
In particular, local traces for re-encryption will contain only a bounded number of re-encryptions for any given ciphertext, leading to a sound elimination of equations that model re-encryption. For associativity and commutativity, local traces will determine a canonical use of the associative-commutative operator, where reasoning modulo AC is no stronger than reasoning without AC.
We illustrate these results by considering a non-disjoint combination of equational theories for the verification of vote privacy in Prêt à Voter. ProVerif can not handle the input theory as it is, but it does terminate with success on the theory obtained using our reduction result.
Original languageEnglish
Title of host publicationPrinciples of Security and Trust
Subtitle of host publicationFirst International Conference, POST 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012, Proceedings
EditorsPierpaolo Degano, JoshuaD. Guttman
PublisherSpringer Berlin Heidelberg
Pages169-188
Number of pages20
ISBN (Electronic)978-3-642-28641-4
ISBN (Print)978-3-642-28640-7
DOIs
Publication statusPublished - 2012

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume7215

Fingerprint

Dive into the research topics of 'Reduction of Equational Theories for Verification of Trace Equivalence: Re-encryption, Associativity and Commutativity'. Together they form a unique fingerprint.

Cite this