Reasoning about Protocols with Human Participants - UMD - October 2015
PI(s): Jonathan Katz, Poorvi L. Vora
Researchers: Hua Wu and Siyuan Feng (graduate students)
HARD PROBLEM(S) ADDRESSED
Hard Problem 5: Understanding and Accounting for Human Behaviour
ACCOMPLISHMENT HIGHLIGHTS
A. Fundamental Research
Our purpose is to rigorously derive security properties of network-security protocols involving human participants and physical objects, where the limited computational capabilities of human participants and the physical properties of the objects affect the security properties of the protocols.
We first consider the example problem of electronic voting. This is an important example because cryptographic voting protocols involving human voters and paper have been used in real governmental elections in the US and in Victoria, Australia. There are efforts (in Travis County, Texas) to use similar protocols in larger elections.
We first consider the example problem of electronic voting. This is an important example because cryptographic voting protocols involving human voters and paper have been used in real governmental elections in the US and in Victoria, Australia. There are efforts (in Travis County, Texas) to use similar protocols in larger elections.
The standard voting model assumes that all interacting parties are computers (probabilistic polynomial-time interactive Turing machines) and can, for example, encrypt and digitally sign messages. Human voters are not explicitly taken into account since it is (implicitly) assumed that each voter has access to a trusted computer while voting. In our work we do not make this assumption, because voters voting from home might have malware on their computers that could be used to throw an election.
Some more recent voting protocols have been designed for human participants voting from untrusted computers, some relying on paper or other physical objects to obtain security guarantees. These protocols have either been used in real governmental elections (the City of Takoma Park, MD, 2009 and 2011---PI Vora was part of the team that deployed the voting system for these elections; vVote in Victoria, Australia, 2014) or are being proposed for such use (STAR-Vote in Travis County, Texas). However, the security properties of these protocols are not well understood. We need a well-developed model to reason about these properties. Such a model would incorporate a human's computational capabilities and the properties of the physical objects. The model would then be used to reason about, and prove security of, the integrity and privacy properties of remote voting protocols such as Remotegrity (used for absentee voting by the City of Takoma Park for its 2011 municipal election).
In the short term, this project will focus on the development of the model of humans and the use of physical obects such as paper, and on the security properties of remote voting protocol Remotegrity. It will also examine possible new protocols that overcome disadvanatages of existing ones for humans. In the longer term---in addition to the general problem of the voting protocol---there are other problems where it is important to consider the fact that all protocol participants are not computers. For example, when a human logs into a website to make a financial transaction (such as a bank website, or a retirement account, or an e-commerce site), the human uses an untrusted computer and hence cannot be expected to correctly encrypt or sign messages. Can one use the techniques developed for electronic voting to develop simple and more secure protocols using physical objects and paper while using the untrusted computer to make the transaction? Can one prove the security properties of the proposed protocols?
Some more recent voting protocols have been designed for human participants voting from untrusted computers, some relying on paper or other physical objects to obtain security guarantees. These protocols have either been used in real governmental elections (the City of Takoma Park, MD, 2009 and 2011---PI Vora was part of the team that deployed the voting system for these elections; vVote in Victoria, Australia, 2014) or are being proposed for such use (STAR-Vote in Travis County, Texas). However, the security properties of these protocols are not well understood. We need a well-developed model to reason about these properties. Such a model would incorporate a human's computational capabilities and the properties of the physical objects. The model would then be used to reason about, and prove security of, the integrity and privacy properties of remote voting protocols such as Remotegrity (used for absentee voting by the City of Takoma Park for its 2011 municipal election).
In the short term, this project will focus on the development of the model of humans and the use of physical obects such as paper, and on the security properties of remote voting protocol Remotegrity. It will also examine possible new protocols that overcome disadvanatages of existing ones for humans. In the longer term---in addition to the general problem of the voting protocol---there are other problems where it is important to consider the fact that all protocol participants are not computers. For example, when a human logs into a website to make a financial transaction (such as a bank website, or a retirement account, or an e-commerce site), the human uses an untrusted computer and hence cannot be expected to correctly encrypt or sign messages. Can one use the techniques developed for electronic voting to develop simple and more secure protocols using physical objects and paper while using the untrusted computer to make the transaction? Can one prove the security properties of the proposed protocols?
B. Accomplishments
In accomplishments this quarter we have completed the specification of a new voting protocol and begun to define its security (privacy and election integrity) properties when voters are human, and multiple terminals and the election server collude to change the election outcome.
C. Community Interaction
PI Vora is part of the technical team for the end-to-end verifiable internet voting (E2E VIV) project (examining the feasibility of secure internet voting) of the overseas vote foundation (OVF). She contributes the observations of this project to the discussions and the report. She has been contributing to a description of end-to-end independently-verifiable cryptographic voting systems meant for non-technical readers including election officials. The project report was released on July 11, 2015: "The Future of Voting: End-to-End Verifiable Internet Voting - Specification and Feasibility Study", see https://www.usvotefoundation.org/E2E-VIV
D. Educational.
None yet.
Groups: