Automated Verification Of Remote Internet Voting Protocols In Applied Pi Calculus

Voting is a way that people express their opinions on something using their right of election. With the development of the technology of computer and communication, it is come true that people vote through Internet voting system in anywhere with computer.Internet voting protocol is the base of the Internet voting system. A secure practical remote Internet voting protocol should include security properties: privacy, completeness, soundness, unreusability, fairness, eligibility, invariableness, DoS-resistance, universal verifiability, receipt-freeness and coercion-resistance.Formal method is a powerful tool of analysis and verification of security properties of security protocols. According to the analysis method, there are two ways: the manual analysis and the automatic analysis. The former relies on expert's experience, not only low efficiency, easy to make a mistake, hard to promote, but also very difficult to apply in analysis of complex protocols. Therefore, automatic technology of analysis and verification of security protocols have been the focus in the field of information security.In this dissertation, remote Internet voting protocols are the research objectives, the formal methods of based on theorem proof of analysis and verification of security protocols is as the tool, automatic technology for proving the security properties of the remote Internet voting protocol are researched.The main work and contribution in this dissertation are summarized as following:1. The first-order theorem prover ProVerif, based on the theorem proof, has been researched deeply. First, the terms, processes and equation relations between processes of applied PI calculus and Horn clause are studied. Those are input languages for ProVerif. Then analysis the ProVerif, including the system structure, basic theory and security properties which it can prove.2. The automatic proof method for the DoS-resistance of remote Internet voting protocol has been researched. A model based on theorem proof for DoS-resistance is proposed. First, the applied calculus is extended from the attacker contexts and process expression, then from the view of protocol state, the protocols are modeled with the extended applied calculus and a automatic method of resistance of denial of service attacks based on theorem proof with first order theorem prover ProVerif is presented, finally resistance of denial of service attacks in Acquisti protocol and IEEE 802.11 4 handshake protocol are analyzed.3. The automatic proof method for receipt-freeness and coercion-resistance of remote Internet voting protocol has been researched. We focus on the Backes model which supports automatic proving soundness, receipt-freeness and coercion-resistance. Then based on the Backes model to analyze and verify the soundness, receipt-freeness and coercion-resistance of Acquisti protocol and Meng protocol. The result we obtained is that Meng protocol is not soundness. We develop the Meng protocol to make sure Meng protocol is soundness.