Abstract
Event-B, a refinement-based formal modelling language, has traditionally focused on safety, but now increasingly finds a new role in developing secure systems. In this paper we take a fresh look at security and focus on what security means for the system rather than looking at detailed protocols. We use Event-B for proving security from an abstract view and refining it towards design details, focusing on the refinement of the availability property of the system. We define a general approach to guarantee the availability of events by ensuring the non-strengthening of their guards, taking into consideration their parameter types. We illustrate our approach using a smart ballot system, an integral part of modern voting systems.
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
Notes
- 1.
We use [Â ] to distinguish rigid events and parameters from others.
- 2.
where [Â ] is a relational image and \(\{\;\mid \;\}\) is a set comprehension. A concise summary of Event-B syntax is available at http://wiki.event-b.org/images/EventB-Summary.pdf.
References
Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)
Abrial, J.-R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. STTT 12(6), 447–466 (2010). https://doi.org/10.1007/s10009-010-0145-y
Börger, E.: The ASM ground model method as a foundation of requirements engineering. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 145–160. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-39910-0_6
Culnane, C., Schneider, S.: A peered bulletin board for robust use in verifiable voting systems. In: 2014 IEEE 27th Computer Security Foundations Symposium (CSF), Los Alamitos, CA, USA, pp. 169–183. IEEE Computer Society (2014)
Galois and Free & Fair: The BESSPIN Voting System, May 2019. https://github.com/GaloisInc/BESSPIN-Voting-System-Demonstrator-2019. Accessed 02 Feb 2021
Gibson, J.P., Kherroubi, S., Méry, D.: Applying a dependency mechanism for voting protocol models using Event-B. In: Bouajjani, A., Silva, A. (eds.) FORTE 2017. LNCS, vol. 10321, pp. 124–138. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-60225-7_9
Hallerstede, S., Hoang, T.S.: Refinement of decomposed models by interface instantiation. Sci. Comput. Program. 94, 144–163 (2014)
Hoang, T. S., Dghaym, D.: Event-B and Rodin Wiki: CamilleX (2018). http://wiki.event-b.org/index.php/CamilleX. Accessed Feb 2021
Leuschel, M., Butler, M.: ProB: a model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45236-2_46
Lowe, G.: Casper: a compiler for the analysis of security protocols. In: Proceedings 10th Computer Security Foundations Workshop, pp. 18–30 (1997)
Schmidt, B., Meier, S., Cremers, C., Basin, D.: Automated analysis of Diffie-Hellman protocols and advanced security properties. In: 2012 IEEE 25th Computer Security Foundations Symposium, pp. 78–94 (2012)
Yadav, D., Butler, M.: Verification of liveness properties in distributed systems. In: Ranka, S., et al. (eds.) IC3 2009. CCIS, vol. 40, pp. 625–636. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03547-0_59
Acknowledgement
This work is supported by the HD-Sec project, which was funded by the Digital Security by Design (DSbD) Programme delivered by UKRI to support the DSbD ecosystem.
We would like to thank Joseph Kiniry and Daniel Zimmerman from Galois for providing details of and insights into the case study.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 Springer Nature Switzerland AG
About this paper
Cite this paper
Dghaym, D., Hoang, T.S., Butler, M., Hu, R., Aniello, L., Sassone, V. (2021). Verifying System-Level Security of a Smart Ballot Box. In: Raschke, A., Méry, D. (eds) Rigorous State-Based Methods. ABZ 2021. Lecture Notes in Computer Science(), vol 12709. Springer, Cham. https://doi.org/10.1007/978-3-030-77543-8_3
Download citation
DOI: https://doi.org/10.1007/978-3-030-77543-8_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-77542-1
Online ISBN: 978-3-030-77543-8
eBook Packages: Computer ScienceComputer Science (R0)