(2019) Automated Verification of Accountability in Security Protocols.
|
Text
accver-conf.pdf Download (468kB) | Preview |
Abstract
Accountability is a recent paradigm in security protocol design which aims to eliminate traditional trust assumptions on parties and hold them accountable for their misbehavior. It is meant to establish trust in the first place and to recognize and react if this trust is violated. In this work, we discuss a protocol-agnostic definition of accountability: a protocol provides accountability (w.r.t. some security property) if it can identify all misbehaving parties, where misbehavior is defined as a deviation from the protocol that causes a security violation. We provide a mechanized method for the verification of accountability and demonstrate its use for verification and attack finding on various examples from the accountability and causality literature, including Certificate Transparency and Kroll’s Accountable Algorithms protocol. We reach a high degree of automation by expressing accountability in terms of a set of trace properties and show their soundness and completeness.
| Item Type: | Conference or Workshop Item (A Paper) (Paper) |
|---|---|
| Additional Information: | distinguished paper |
| Divisions: | Michael Backes (InfSec) |
| Conference: | CSF IEEE Computer Security Foundations Symposium (was CSFW) |
| Depositing User: | Robert Künnemann |
| Date Deposited: | 07 Jun 2019 06:58 |
| Last Modified: | 18 Jul 2019 11:52 |
| Primary Research Area: | NRA2: Reliable Security Guarantees |
| URI: | https://publications.cispa.saarland/id/eprint/2896 |
Actions
Actions (login required)
 |
View Item |