Reasoning about Protocols with Human Participants - UMD - October 2014
Public Audience
Purpose: To highlight project progress. Information is generally at a higher level which is accessible to the interested public. All information contained in the report (regions 1-3) is a Government Deliverable/CDRL.
PI(s): Jonathan Katz, Poorvi L. Vora
Researchers: Hua Wu (graduate student)
HARD PROBLEM(S) ADDRESSED
This refers to Hard Problems, released November 2012.
Hard Problem 5: Understanding and Accounting for Human Behaviour
PUBLICATIONS
Papers published in this quarter as a result of this research. Include title, author(s), venue published/presented, and a short description or abstract. Identify which hard problem(s) the publication addressed. Papers that have not yet been published should be reported in region 2 below.
None yet
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 voting protocols have been used in real (albeit small) governmental elections in the US, and there are efforts (in Travis County, Texas and Victoria, Australia) 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) or are being proposed for such use (vVote in Victoria, Australia, 2014, and 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. 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?
We first consider the example problem of electronic voting. This is an important example because voting protocols have been used in real (albeit small) governmental elections in the US, and there are efforts (in Travis County, Texas and Victoria, Australia) 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) or are being proposed for such use (vVote in Victoria, Australia, 2014, and 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. 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 to date, we have begun formally specifying two remote voting protocols: Remotegrity and Helios. The former uses paper, while the latter does not. The former appears to be ``more secure'' --- in particular, with the ability to resolve disputes between the voting system or voting computer, which might claim that it encrypted the vote correctly, and the voter, who might dispute this claim. This project is rigorously examining this difference between the two protocols.
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. In the most recent quarter, she has been contributing to a description of end-to-end independently-verifiable cryptographic voting systems meant for non-technical readrs including election officials.
D. Educational.
None yet.