Formal Specification and Analysis of an Evoting System


	BibTex \| RIS \| RefWorks Download

, ,

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 e- voting systems show serious specification, design, and imple- mentation,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 Develop- ment,Environment,(SDE). The PVS interactive theorem,prover was,then used,to apply,the appropriate,proof strategies and

Conference: Availability, Reliability and Security - IEEEARES , pp. 164-171, 2010

DOI: 10.1109/ARES.2010.83

Cumulative Annual

View Publication