Abstract
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 language | English |
|---|---|
| Title of host publication | Proceedings of the 2022 IEEE 35th Computer Security Foundations Symposium (CSF) |
| Publisher | IEEE |
| Publication date | 2022 |
| Pages | 130-146 |
| ISBN (Print) | 978-1-6654-8418-3 |
| ISBN (Electronic) | 978-1-6654-8417-6 |
| DOIs | |
| Publication status | Published - 2022 |
| Event | 2022 IEEE 35th Computer Security Foundations Symposium - Haifa, Israel Duration: 7 Aug 2022 → 10 Aug 2022 Conference number: 35 |
Conference
| Conference | 2022 IEEE 35th Computer Security Foundations Symposium |
|---|---|
| Number | 35 |
| Country/Territory | Israel |
| City | Haifa |
| Period | 07/08/2022 → 10/08/2022 |
Keywords
- Formal Methods
- Protocol security
- Transition system
- Linkability
- DP-3T