Privacy as Reachability

Sebastien Gondron, Sebastian Moedersheim, Luca Viganò

Research output: Chapter in Book/Report/Conference proceedingConference paperpeer-review

139 Downloads (Pure)


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.
Original languageEnglish
Title of host publication35th IEEE Computer Security Foundations Symposium (CSF 2022)
PublisherIEEE Computer Society Press
Number of pages17
Publication statusPublished - 31 May 2022


Dive into the research topics of 'Privacy as Reachability'. Together they form a unique fingerprint.

Cite this