Static validation of voting protocols |
E. H. Andersen, C. R. 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 |
| Note | Supervised by Prof. Hanne Riis Nielson |
| Publication link | http://www2.imm.dtu.dk/pubdb/p.php?3968 |
| BibTeX data | [bibtex] |
| IMM Group(s) | Computer Science & Engineering |