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.
|Title of host publication||35th IEEE Computer Security Foundations Symposium (CSF 2022)|
|Publisher||IEEE Computer Society Press|
|Number of pages||17|
|Publication status||Published - 31 May 2022|