VERIFIKASI COERCION-RESISTANCE ELECTRONIC VOTING PROTOCOL MENGGUNAKAN APPLIED �-CALCULUS

Coercion-resistance becomes major property must be fulfilled by Internet-based voting scheme because it is believed to be able to capture all behaviors that may be conducted by the attacker. Electronic voting protocol which is coercion-resistance is a protocol that has immunity to simulation attack, randomization attack, and forced-abstention attack. Verification of electronic voting protocol means specifying and verifying a system by using techniques, tools, and languages based on mathematic. Formal mathematical language being used in this research is applied �-calculus, which is a variant of language in process calculi to model distributed system and its entities' interaction. Verification using applied �-calculus can be proved by using manual technique or automated tools like ProVerif. Coercion-resistance protocol being verified is a protocol proposed by Stefan G. Weber which its prototype implementation exhibits a linear runtime with the number of votes. Therefor this protocol can be used in the real world large scale election. The result of the protocol verification is proving that the protocol can not satisfy coercion-resistance in immunity of simulation attack, those there is no possibility for a voter to cheat a coercer by giving him a fake secret identity to cast a vote on voter's behalf