Formal Specification of a Security Protocol for Internet Voting
Take any existing protocol or (open source) system for Internet Voting, reverse engineer it to write a full specification in BON and JML. List and explain the desirable security properties of a perfect remote voting system. Find and prove at least one security property that is violated by the protocol or software package that you have chosen. You must find at least one security weakness not already discovered or published. Ideally you would find two or three major flaws in the system.
- Supervisor Dermot Cochran
- Subject Area software engineering
- Pre-requisites strong knowledge of Java and strong programming skills
- Co-requisites (things you must learn along the way) Voting systems and electoral law, the Java Modeling Language, the JML tool suite, ESC/Java2
- Subject Coverage software engineering with applied formal methods
- Project Type formal system design and specification
- Hardware/Software PC, laptop or workstation capable of running Java and Eclipse
Description
Take any existing protocol or (open source) system for Internet Voting, reverse engineer it to write a full specification in BON and JML
Mandatory Goals
- Become familiar with Internet voting.
- List and explain the desirable security properties of a perfect remote voting system.
- Find and prove at least one security property that is violated by the protocol or software package that you have chosen. You must find at least one security weakness not already discovered or published. Ideally you would find two or three major flaws in the system.
Discretionary Goals
- Ideally you would find two or three major flaws in the system. .
Exceptional Goals
- Coauthor, submit, and publish a paper on this work.
- Specify and prove some (behavioral and security) properties about the specification.