Static validation of voting protocols |
Esben Heltoft Andersen, Christoffer Rosenkilde Nielsen
|
| Abstract | Previous studies have shown that language based technologies can be used to automatically validate classical protocols. In this thesis we shall apply these methods to a different type of protocols; namely electronic voting protocols.
We shall study three voting protocols; FOO92, Sensus and E-vox. These are modelled in the process calculus LYSA and validated using the corresponding analysis. However, as the protocols utilise cryptographic operations which are not incorporated into LYSA, we shall extend the calculus and the analysis. This extension is proven sound with respect to the semantics and the corresponding implementation is proven sound with respect to the analysis.
The difficulties concerning the modelling of the voting protocols in LYSA, stresses the need for LYSA XP ; a process calculus and a corresponding analysis, which we present in the second part of the thesis. The analysis of LYSA XP is also proven sound with respect to the semantics. |
| Type | Master's thesis [Academic thesis] |
| Year | 2005 |
| Publisher | Informatics and Mathematical Modelling, Technical University of Denmark, DTU |
| Address | Richard Petersens Plads, Building 321, DK-2800 Kgs. Lyngby |
| Series | IMM-Thesis-2005-55 |
| Note | Supervised by Prof. Hanne Riis Nielson |
| Electronic version(s) | [pdf] |
| BibTeX data | [bibtex] |
| IMM Group(s) | Computer Science & Engineering |