Reasoning about Protocols with Human Participants - UMD - April 2015
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 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. 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. 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, and have made changes to simplify the former and improve its security properties. The former protocol uses "scratch-off cards," 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, for example, claim that it cast the vote correctly) and the voter (who might dispute this claim). This project is rigorously examining this difference between the two protocols. We have also examined the differences between Remotegrity and in-person voting protocols that use paper and scratch-off cards.
We are in the process of formally specifying a model in which to prove security, and writing up a proof of security for the Remotegrity protocol.
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.
PI Vora was invited to participate in the plenary panel: "Blue Skies / Blank Check" at the annual conference of the Election Verification Network (EVN), which is a nonpartisan network of professionals committed to election integrity. Its membership includes "voting activists, computer scientists, election law and voting rights attorneys, academic experts, election officials, civil rights advocates and more". Attendance at the conference was open to EVN members and invited guests only.
PI Vora was quoted in the Washington Post: Amrita Jayakumar, "Can you vote for the next president on your smartphone? Not just yet." Washington Post, April 6, 2015, Pg. A13.
PI Vora spoke about this project at the lablet quarterly meeting in January that was held in Raleigh.
D. Educational.
None yet.
Groups: