Privacy by Design: On the Conformance Between Protocols and Architectures

TL;DR

This paper introduces a formal method to verify if concrete privacy protocols conform to high-level privacy architectures, bridging the gap between system design and implementation.

Contribution

It proposes a process algebra variant for modeling protocols and a mapping procedure to check conformance to privacy architectures.

Findings

Formal verification of protocol conformance to architectures

A process algebra framework for privacy protocol analysis

Mapping procedures linking protocols to high-level architectures

Abstract

In systems design, we generally distinguish the architecture and the protocol levels. In the context of privacy by design, in the first case, we talk about privacy architectures, which define the privacy goals and the main features of the system at high level. In the latter case, we consider the underlying concrete protocols and privacy enhancing technologies that implement the architectures. In this paper, we address the question that whether a given protocol conforms to a privacy architecture and provide the answer based on formal methods. We propose a process algebra variant to define protocols and reason about privacy properties, as well as a mapping procedure from protocols to architectures that are defined in a high-level architecture language.