Automated Analysis of Accountability
Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review
Standard
Automated Analysis of Accountability. / Bruni, Alessandro; Giustolisi, Rosario; Schürmann, Carsten.
Information Security - 20th International Conference, {ISC} 2017, Ho Chi Minh City, Vietnam, November 22-24, 2017, Proceedings. Springer, 2017. p. 417-434 (Lecture Notes in Computer Science, Vol. 10599).Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - GEN
T1 - Automated Analysis of Accountability
AU - Bruni, Alessandro
AU - Giustolisi, Rosario
AU - Schürmann, Carsten
PY - 2017
Y1 - 2017
N2 - A recent trend in the construction of security protocols such as voting and certificate management systems is to make principals accountable for their actions. Whenever some principals deviate from the protocol’s prescription and cause the failure of a goal of the system, accountability ensures that the system can detect the misbehaving parties who caused that failure. Accountability is an intuitively stronger property than verifiability as the latter only rests on the possibility of detecting the failure of a goal. A plethora of accountability and verifiability definitions have been proposed in the literature. Those definitions are either very specific to the protocols in question, hence not applicable in other scenarios, or too general and widely applicable but requiring complicated and hard to follow manual proofs.In this paper, we advance formal definitions of verifiability and accountability that are amenable to automated verification. Our definitions are general enough to be applied to different classes of protocols and different automated security verification tools. Furthermore, we point out formally the relation between verifiability and accountability. We validate our definitions with the automatic verification of three protocols: a secure exam protocol, Google’s Certificate Transparency, and an improved version of Bingo Voting. We find through automated verification that all three protocols satisfy verifiability while only the first two protocols meet accountability.
AB - A recent trend in the construction of security protocols such as voting and certificate management systems is to make principals accountable for their actions. Whenever some principals deviate from the protocol’s prescription and cause the failure of a goal of the system, accountability ensures that the system can detect the misbehaving parties who caused that failure. Accountability is an intuitively stronger property than verifiability as the latter only rests on the possibility of detecting the failure of a goal. A plethora of accountability and verifiability definitions have been proposed in the literature. Those definitions are either very specific to the protocols in question, hence not applicable in other scenarios, or too general and widely applicable but requiring complicated and hard to follow manual proofs.In this paper, we advance formal definitions of verifiability and accountability that are amenable to automated verification. Our definitions are general enough to be applied to different classes of protocols and different automated security verification tools. Furthermore, we point out formally the relation between verifiability and accountability. We validate our definitions with the automatic verification of three protocols: a secure exam protocol, Google’s Certificate Transparency, and an improved version of Bingo Voting. We find through automated verification that all three protocols satisfy verifiability while only the first two protocols meet accountability.
U2 - 10.1007/978-3-319-69659-1_23
DO - 10.1007/978-3-319-69659-1_23
M3 - Article in proceedings
SN - 978-3-319-69658-4
T3 - Lecture Notes in Computer Science
SP - 417
EP - 434
BT - Information Security - 20th International Conference, {ISC} 2017, Ho Chi Minh City, Vietnam, November 22-24, 2017, Proceedings
PB - Springer
ER -
ID: 82351956