Skip to Main content Skip to Navigation
New interface
Conference papers

Formal verification of tamper-evident storage for e-voting

Dominique Cansell 1 Paul Gibson 1 Dominique Méry 1, * 
* Corresponding author
1 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : The storage of votes is a critical component of any voting system. In traditional systems there is a high level of transparency in the mechanisms used to store votes, and thus a reasonable degree of trustworthiness in the security of the votes in storage. This degree of transparency is much more difficult to attain in electronic voting systems, and so the specific mechanisms put in place to ensure the security of stored votes require much stronger verification in order for them to be trusted by the public. There are many desirable properties that one could reasonably expect a vote store to exhibit. From the point of view of security, we argue that {\it tamper-evident} storage is one of the most important requirements: the changing, or deletion of already validated and stored votes should be detectable; as should the addition of unauthorised votes after the election is concluded. We propose the application of formal methods (in this paper, event-B) for guaranteeing, through construction, the correctness of a vote store with respect to the requirement for {\it tamper-evident} storage. We illustrate the utility of our refinement-based approach by verifying --- through the application of a reusable formal design pattern --- a store design that uses a specific PROM technology and applies a specific encoding mechanism.
Document type :
Conference papers
Complete list of metadata

Cited literature [22 references]  Display  Hide  Download
Contributor : Dominique Méry Connect in order to contact the contributor
Submitted on : Friday, November 2, 2007 - 11:16:34 AM
Last modification on : Friday, February 4, 2022 - 3:22:09 AM
Long-term archiving on: : Monday, September 24, 2012 - 2:50:08 PM


Files produced by the author(s)




Dominique Cansell, Paul Gibson, Dominique Méry. Formal verification of tamper-evident storage for e-voting. 5th IEEE International Conference on Software Engineering and Formal Methods - SEFM 2007, Sep 2007, LONDON, United Kingdom. pp.329-338, ⟨10.1109/SEFM.2007.21⟩. ⟨inria-00184833⟩



Record views


Files downloads