Author | Conference | Journal | Organization | Year | DOI
Look for results that meet for the following criteria:
Academic
Publications
Formal verification of tamper-evident storage for e-voting
Edit
Formal verification of tamper-evident storage for e-voting   (Citations: 8)
BibTex | RIS | RefWorks Download
The storage of votes is a critical component of any voting system. In traditional systems there is a high level of trans- parency 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 tamper-evident storage is one of the most important require- ments: 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 pro- pose 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 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.
Conference: Conference on Software Engineering and Formal Methods - SEFM , pp. 329-338, 2007
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
More »
    • ...A secondary objective is to demonstrate the application of formal methods — as in [5,6] — in the engineering of the software in the e-voting system, which we consider to be critical[24]...

    J. Paul Gibson, et al. Engineering a Distributed eVoting System Architecture: Meeting Critica...

    • ...Integrating SPL techniques with formal methods is a promising approach: refinement for re-use of trustworthy components has already been addressed with respect to e-voting machine interfaces [22] and storage [29]...
    • ...Current research — based on the notion of a feature interaction algebra[31] — suggests that a correct-by-construction approach to guaranteeing the functionality of evoting systems[22,29] merits further investigation...

    J. Paul Gibson, et al. Feature Interactions in a Software Product Line for Evoting

    • ...In previous works, we have already identified techniques for paramatrised development of B models; formal verification of tamper-evident storage for e-voting [22] and the incremental parametric development of greedy algorithms [27], are applying a technique jointly developed with J.-R...
    • ...• The parametric/generic pattern provides a way to instantiate Event B development and we apply it on two very different case studies: the design of greedy algorithms [27] and the design of e-voting algorithms [22, 21]...

    Projet RIMEL. Livrable 3 Proof-based design patterns

    • ...See, respectively, [15], [16], [17], [18] and [19], [20], [21], [22], [23], [24] research efforts to improve the current design of e-voting systems and their critiques...

    Komminist Weldemariam, et al. Managing Requirements for EVoting Systems: Issues and Approaches

    • ...Cansell et al. [1, 2] recommend application of formal methods for guaranteeing tamper-evident storage of votes and secure voting machine interface development...

    J. Paul Gibson, et al. Analysis of a Distributed eVoting System Architecture against Quality ...

Order by:

Citations (8)

Share this on | Contribute to Academic