Abstract
We present a decision procedure for verifying whether a protocol respects privacy goals, given a bound on the number of transitions. We consider multi message-analysis problems, where the intruder does not know exactly the structure of the messages but rather knows several possible structures and that the real execution corresponds to one of them. This allows for modeling a large class of security protocols, with standard cryptographic operators, non-determinism and branching. Our main contribution is the definition of a decision procedure for a fragment of alpha-beta privacy. Moreover, we have implemented a prototype tool as a proof-of-concept and a first step towards automation.
| Original language | English |
|---|---|
| Title of host publication | Proceedings of the 37th IEEE Computer Security Foundations Symposium (CSF 2024) |
| Publisher | IEEE |
| Publication date | 2024 |
| Pages | 17-32 |
| DOIs | |
| Publication status | Published - 2024 |
| Event | 2024 IEEE 37th Computer Security Foundations Symposium - Enschede, Netherlands Duration: 8 Jul 2024 → 12 Jul 2024 Conference number: 37 |
Conference
| Conference | 2024 IEEE 37th Computer Security Foundations Symposium |
|---|---|
| Number | 37 |
| Country/Territory | Netherlands |
| City | Enschede |
| Period | 08/07/2024 → 12/07/2024 |
Keywords
- Privacy
- Security Protocols
- Unlinkability
- Formal Methods
- Automated Verification