Privacy as Reachability

TY - CHAP

T1 - Privacy as Reachability

AU - Gondron, Sebastien

AU - Moedersheim, Sebastian

AU - Viganò, Luca

PY - 2022/5/31

Y1 - 2022/5/31

N2 - We show that privacy can be formalized as a reachability problem. We introduce a transaction-process formalism for distributed systems that can exchange cryptographic messages (in a black-box cryptography model). Our formalism includes privacy variables chosen non-deterministically from finite domains (e.g., candidates in a voting protocol), it can work with long-term mutable states (e.g., a hash-key chain) and allows one to specify consciously released information (e.g., number of votes and the result). We discuss examples, e.g., problems of linkability, and the core of the privacy-preserving proximity tracing system DP-3T.

AB - We show that privacy can be formalized as a reachability problem. We introduce a transaction-process formalism for distributed systems that can exchange cryptographic messages (in a black-box cryptography model). Our formalism includes privacy variables chosen non-deterministically from finite domains (e.g., candidates in a voting protocol), it can work with long-term mutable states (e.g., a hash-key chain) and allows one to specify consciously released information (e.g., number of votes and the result). We discuss examples, e.g., problems of linkability, and the core of the privacy-preserving proximity tracing system DP-3T.

M3 - Conference paper

BT - 35th IEEE Computer Security Foundations Symposium (CSF 2022)

PB - IEEE Computer Society Press

ER -