Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Cortier, V., Galindo, D., Küsters, R., Müller, J., Truderung, T.: SoK: verifiability notions for e-voting protocols. In: 2016 IEEE Symposium on Security and Privacy (SP), pp. 779–798 (2016)
Küsters, R., Truderung, T., Vogt, A.: Accountability: definition and relationship to verifiability. In: Proceedings of the 17th ACM Conference on Computer and Communications Security, CCS 2010, pp. 526–535. ACM, New York (2010)
Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: CSFW, pp. 82–96. IEEE Computer Society (2001)
Mödersheim, S., Bruni, A.: AIF-\(\omega \): set-based protocol abstraction with countable families. In: Piessens, F., Viganò, L. (eds.) POST 2016. LNCS, vol. 9635, pp. 233–253. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49635-0_12
Milner, K., Cremers, C.J.F., Yu, J., Ryan, M.: Automatically detecting the misuse of secrets: Foundations, design principles, and applications. IACR Cryptol. ePrint Arch. 234 (2017)
Jagadeesan, R., Jeffrey, A., Pitcher, C., Riely, J.: Towards a theory of accountability and audit. In: Backes, M., Ning, P. (eds.) ESORICS 2009. LNCS, vol. 5789, pp. 152–167. Springer, Heidelberg (2009). doi:10.1007/978-3-642-04444-1_10
Bella, G., Paulson, L.C.: Accountability protocols: formalized and verified. ACM Trans. Inf. Syst. Secur. 9, 138–161 (2006)
Zhou, J., Gollmann, D.: A fair non-repudiation protocol. In: Proceedings of the 1996 IEEE Conference on Security and Privacy, SP 1996, pp. 55–61. IEEE Computer Society, Washington, DC (1996)
Abadi, M., Blanchet, B.: Computer-assisted verification of a protocol for certified email. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 316–335. Springer, Heidelberg (2003). doi:10.1007/3-540-44898-5_17
Kremer, S., Ryan, M., Smyth, B.: Election verifiability in electronic voting protocols. In: Gritzalis, D., Preneel, B., Theoharidou, M. (eds.) ESORICS 2010. LNCS, vol. 6345, pp. 389–404. Springer, Heidelberg (2010). doi:10.1007/978-3-642-15497-3_24
Benaloh, J., Tuinstra, D.: Receipt-free secret-ballot elections (extended abstract). In: Proceedings of the 26th Symposium on Theory of Computing (STOC 1994), pp. 544–553. ACM, New York (1994)
Hirt, M., Sako, K.: Efficient receipt-free voting based on homomorphic encryption. In: Preneel, B. (ed.) EUROCRYPT 2000. LNCS, vol. 1807, pp. 539–556. Springer, Heidelberg (2000). doi:10.1007/3-540-45539-6_38
Cohen, J., Fischer, M.: A robust and verifiable cryptographically secure election scheme (extended abstract). In: Proceedings of the 26th Annual Symposium on Foundations of Computer Science (FOCS 1985), Portland, Oregon, USA, pp. 372–382. IEEE Computer Society (1985)
Benaloh, J.: Verifiable Secret-Ballot Elections. Ph.D. thesis, Yale University (1996)
Smyth, B., Ryan, M., Kremer, S., Kourjieh, M.: Towards automatic analysis of election verifiability properties. In: Armando, A., Lowe, G. (eds.) ARSPA-WITS 2010. LNCS, vol. 6186, pp. 146–163. Springer, Heidelberg (2010). doi:10.1007/978-3-642-16074-5_11
Dreier, J., Jonker, H., Lafourcade, P.: Defining verifiability in e-auction protocols. In: Proceedings of the 8th ACM Symposium on Information, Computer and Communications Security (ASIACCS 2013), Hangzhou, China, pp. 547–552. ACM (2013)
Guts, N., Fournet, C., Zappa Nardelli, F.: Reliable evidence: auditability by typing. In: Backes, M., Ning, P. (eds.) ESORICS 2009. LNCS, vol. 5789, pp. 168–183. Springer, Heidelberg (2009). doi:10.1007/978-3-642-04444-1_11
Bella, G., Giustolisi, R., Lenzini, G., Ryan, P.Y.: Trustworthy exams without trusted parties. Comput. Secur. 67, 291–307 (2017)
Laurie, B., Langley, A., Kasper, E.: Certificate transparency. Technical report (2013)
Merkle, R.C.: A digital signature based on a conventional encryption function. In: Pomerance, C. (ed.) CRYPTO 1987. LNCS, vol. 293, pp. 369–378. Springer, Heidelberg (1988). doi:10.1007/3-540-48184-2_32
Bohli, J.-M., Müller-Quade, J., Röhrich, S.: Bingo voting: secure and coercion-free voting using a trusted random number generator. In: Alkassar, A., Volkamer, M. (eds.) Vote-ID 2007. LNCS, vol. 4896, pp. 111–124. Springer, Heidelberg (2007). doi:10.1007/978-3-540-77493-8_10
Bohli, J.M., Henrich, C., Kempka, C., Muller-Quade, J., Rohrich, S.: Enhancing electronic voting machines on the example of bingo voting. IEEE Trans. Inf. Forensics Secur. 4, 745–750 (2009)
Jakobsson, M., Juels, A., Rivest, R.L.: Making mix nets robust for electronic voting by randomized partial checking. In: Proceedings of the 11th USENIX Security Symposium, Berkeley, CA, USA, pp. 339–353. USENIX Association (2002)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Bruni, A., Giustolisi, R., Schuermann, C. (2017). Automated Analysis of Accountability. In: Nguyen, P., Zhou, J. (eds) Information Security. ISC 2017. Lecture Notes in Computer Science(), vol 10599. Springer, Cham. https://doi.org/10.1007/978-3-319-69659-1_23
Download citation
DOI: https://doi.org/10.1007/978-3-319-69659-1_23
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-69658-4
Online ISBN: 978-3-319-69659-1
eBook Packages: Computer ScienceComputer Science (R0)