Abstract
We develop and explain the design decisions of a framework for the formal specification and analysis of interactions in generalized distributed systems. Our approach is suitable to reason about various types of agents and supports the modeling of synchronous interactions between any finite number of agents. Our proposal provides a common ground for existing modeling techniques for cryptographic protocols and security ceremonies, by generalizing and unifying them in a single formalism. We discuss the specification of security properties in our framework and demonstrate on a short voting ceremony a technique to model our ceremonies in the Tamarin prover.
| Original language | English |
|---|---|
| Title of host publication | 37th IEEE Computer Security Foundations Symposium (CSF) |
| Publisher | IEEE |
| Pages | 464-478 |
| Number of pages | 15 |
| ISBN (Electronic) | 9798350362039 |
| DOIs | |
| Publication status | Published - 20 Sept 2024 |
| Event | 37th IEEE Computer Security Foundations Symposium 2024 - Enschede, Netherlands Duration: 8 Jul 2024 → 12 Jul 2024 |
Conference
| Conference | 37th IEEE Computer Security Foundations Symposium 2024 |
|---|---|
| Abbreviated title | CSF 2024 |
| Country/Territory | Netherlands |
| City | Enschede |
| Period | 8/07/24 → 12/07/24 |
Keywords
- ceremony
- formal modeling
- security protocol
- specification
- verification
ASJC Scopus subject areas
- General Engineering