Verifying System-Level Security of a Smart Ballot Box

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.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{DghaymHBHAS21,
  author       = {Dana Dghaym and
                  Thai Son Hoang and
                  Michael J. Butler and
                  Runshan Hu and
                  Leonardo Aniello and
                  Vladimiro Sassone},
  editor       = {Alexander Raschke and
                  Dominique M{\'{e}}ry},
  title        = {Verifying System-Level Security of a Smart Ballot Box},
  booktitle    = {Rigorous State-Based Methods - 8th International Conference, {ABZ}
                  2021, Ulm, Germany, June 9-11, 2021, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {12709},
  pages        = {34--49},
  publisher    = {Springer},
  year         = {2021},
  url          = {https://doi.org/10.1007/978-3-030-77543-8\_3},
  doi          = {10.1007/978-3-030-77543-8\_3},
  timestamp    = {Wed, 09 Jun 2021 12:14:31 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/DghaymHBHAS21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}