Skip to main content

Verifying Privacy-Type Properties in a Modular Way

Arapinis, Myrto, Cheval, Vincent, Delaune, Stéphanie (2012) Verifying Privacy-Type Properties in a Modular Way. In: 25th IEEE Computer Security Foundations Symposium (CSF'12), June 2012, Cambridge Massachusetts, USA. (doi:10.1109/CSF.2012.16) (KAR id:46728)

PDF Publisher pdf
Language: English
Download (288kB) Preview
[thumbnail of ACD-csf12.pdf]
Preview
This file may not be suitable for users of assistive technology.
Request an accessible format
PDF (The long version of the paper) Supplemental Material
Language: English
Download (541kB) Preview
[thumbnail of The long version of the paper]
Preview
This file may not be suitable for users of assistive technology.
Request an accessible format
Official URL
http://dx.doi.org/10.1109/CSF.2012.16

Abstract

Formal methods have proved their usefulness for analysing the security of protocols. In this setting, privacy-type security properties (e.g. vote-privacy, anonymity, unlink ability) that play an important role in many modern applications are formalised using a notion of equivalence. In this paper, we study the notion of trace equivalence and we show how to establish such an equivalence relation in a modular way. It is well-known that composition works well when the processes do not share secrets. However, there is no result allowing us to compose processes that rely on some shared secrets such as long term keys. We show that composition works even when the processes share secrets provided that they satisfy some reasonable conditions. Our composition result allows us to prove various equivalence-based properties in a modular way, and works in a quite general setting. In particular, we consider arbitrary cryptographic primitives and processes that use non-trivial else branches. As an example, we consider the ICAO e-passport standard, and we show how the privacy guarantees of the whole application can be derived from the privacy guarantees of its sub-protocols.

Item Type: Conference or workshop item (Paper)
DOI/Identification number: 10.1109/CSF.2012.16
Uncontrolled keywords: Cryptographic protocols, Formal verification, Symbolic model, Composition, Equivalence properties, Reachability properties
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: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Vincent Cheval
Date Deposited: 23 Jan 2015 11:25 UTC
Last Modified: 16 Feb 2021 13:22 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/46728 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year