Formal verification of tamper-evident storage for e-voting

Dominique Cansell 1 Paul Gibson 1 Dominique Méry 1, *
* Auteur correspondant
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.
Type de document :
Communication dans un congrès
Mike Hinchey and Tiziana Margaria. 5th IEEE International Conference on Software Engineering and Formal Methods - SEFM 2007, Sep 2007, LONDON, United Kingdom. IEEE, pp.329-338, 2007, Fifth IEEE International Conference on Software Engineering and Formal Methods, 2007. SEFM 2007. 〈10.1109/SEFM.2007.21〉
Liste complète des métadonnées

Littérature citée [22 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00184833
Contributeur : Dominique Méry <>
Soumis le : vendredi 2 novembre 2007 - 11:16:34
Dernière modification le : jeudi 11 janvier 2018 - 06:19:52
Document(s) archivé(s) le : lundi 24 septembre 2012 - 14:50:08

Fichier

mery-e-voting.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

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

Partager

Métriques

Consultations de la notice

255

Téléchargements de fichiers

171