cispa_all_3447.pdf (452.9 kB)

Verifying Accountability for Unbounded Sets of Participants

Download (452.9 kB)
conference contribution
posted on 2023-11-29, 18:16 authored by Kevin MorioKevin Morio, Robert KünnemannRobert Künnemann
Little can be achieved in the design of security protocols without trusting at least some participants. This trust should be justified or, at the very least, subject to examination. One way to strengthen trustworthiness is to hold parties accountable for their actions, as this provides a strong incentive to refrain from malicious behavior. This has led to an increased interest in accountability in the design of security protocols. In this work, we combine the accountability definition of Künnemann et al. with the notion of case tests to extend its applicability to protocols with unbounded sets of participants. We propose a general construction of verdict functions and a set of verification conditions that achieve soundness and completeness. Expressing the verification conditions in terms of trace properties allows us to extend Tamarin---a protocol verification tool---with the ability to analyze and verify accountability properties in a highly automated way. In contrast to prior work, our approach is significantly more flexible and applicable to a wider range of protocols.


Preferred Citation

Kevin Morio and Robert Künnemann. Verifying Accountability for Unbounded Sets of Participants. In: IEEE Computer Security Foundations Symposium (CSF). 2021.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

IEEE Computer Security Foundations Symposium (CSF)

Legacy Posted Date


Open Access Type

  • Green


@inproceedings{cispa_all_3447, title = "Verifying Accountability for Unbounded Sets of Participants", author = "Morio, Kevin and Künnemann, Robert", booktitle="{IEEE Computer Security Foundations Symposium (CSF)}", year="2021", }

Usage metrics


    No categories selected


    Ref. manager