Skip to Main content Skip to Navigation
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 metadatas

Cited literature [22 references]  Display  Hide  Download

https://hal.inria.fr/inria-00184833
Contributor : Dominique Méry <>
Submitted on : Friday, November 2, 2007 - 11:16:34 AM
Last modification on : Tuesday, February 18, 2020 - 3:28:53 PM
Document(s) archivé(s) le : Monday, September 24, 2012 - 2:50:08 PM

File

mery-e-voting.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

301

Files downloads

457