CINECA IRIS Institutional Research Information System
IRIS è l’archivio della produzione scientifica della Fondazione Bruno Kessler.
EnglishElectronic voting systems are a perfect example of security-critical computing. One of the critical and complex parts of such systems is the voting process, which is responsible for correctly and securely storing intentions and actions of the voters. Unfortunately, recent studies revealed that various evoting systems show serious specification, design, and implementation flaws. The application of formal specification and verification can greatly help to better understand the system requirements of e-voting systems by thoroughly specifying and analyzing the underlying assumptions and the security specific properties. This paper presents the specification and verification of the electronic voting process for the Election Systems & Software (ES&S) system. We used the ASTRAL language to specify the voting process of ES&S machines and the critical security requirements for the system. Proof obligations that verify that the specified system meets the critical requirements were automatically generated by the ASTRAL Software Development Environment (SDE). The PVS interactive theorem prover was then used to apply the appropriate proof strategies and discharge the proof obligations.
Scheda prodotto non validato
Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte di FBK.
| Titolo: | Formal Specification and Analysis of an e-Voting System |
| Autori: | |
| Data di pubblicazione: | 2010 |
| Abstract: | Electronic voting systems are a perfect example of security-critical computing. One of the critical and complex parts of such systems is the voting process, which is responsible for correctly and securely storing intentions and actions of the voters. Unfortunately, recent studies revealed that various evoting systems show serious specification, design, and implementation flaws. The application of formal specification and verification can greatly help to better understand the system requirements of e-voting systems by thoroughly specifying and analyzing the underlying assumptions and the security specific properties. This paper presents the specification and verification of the electronic voting process for the Election Systems & Software (ES&S) system. We used the ASTRAL language to specify the voting process of ES&S machines and the critical security requirements for the system. Proof obligations that verify that the specified system meets the critical requirements were automatically generated by the ASTRAL Software Development Environment (SDE). The PVS interactive theorem prover was then used to apply the appropriate proof strategies and discharge the proof obligations. |
| Handle: | http://hdl.handle.net/11582/5274 |
| Appare nelle tipologie: | 4.1 Contributo in Atti di convegno |
File in questo prodotto:
http://hdl.handle.net/11582/5274
Copyright © 2020