Beta 1


Title Static validation of voting protocols
Author Andersen, Esben Heltoft
Nielsen, Christoffer Rosenkilde (Department of Informatics and Mathematical Modeling, Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark)
Nielson, Hanne Riis (Department of Informatics and Mathematical Modeling, Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark)
Institution Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark
Thesis level Master's thesis
Year 2005
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.
Imprint Department of Informatics and Mathematical Modeling, Technical University of Denmark, DTU : DK-2800 Kgs. Lyngby, Denmark
Pages 143
Fulltext
Original PDF imm3968.pdf (0.80 MB)
Admin Creation date: 2006-06-22    Update date: 2012-12-19    Source: dtu    ID: 185816    Original MXD