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

REZANIA AGRAMANISTI AZDY, Dr.-Ing. MHD. Reza M.I. Pulungan, S.Si., M.Sc.

2013 | Tesis | S2 Ilmu Komputer

Coercion-resistance menjadi properti utama yang harus dimiliki oleh Internet-based voting karena diyakini mampu menangkap segala perilaku yang mungkin dilakukan oleh attacker . Protokol electronic voting yang coercioresistance adalah protokol yang memiliki ketahanan terhadap simulation attack, randomization attack, dan forced-abstention attack. Verifikasi protokol electronic voting (secara formal) berarti menspesifikasikan dan memverifikasi sebuah sistem dengan menggunakan teknik, tool, dan bahasa yang matematis. Verifikasi dilakukan untuk memeriksa apakah sebuah protokol electronic voting dapat memenuhi properti yang dikehendaki atau tidak. Bahasa matematis formal yang digunakan dalam penelitian ini adalah applied π-calculus, yaitu salah satu varian bahasa dalam proses aljabar untuk memodelkan sistem yang terdistribusi dan interaksi antar entitas pada sistem tersebut. Verifikasi dengan menggunakan applied π-calculus dapat dibuktikan dengan menggunakan teknik manual maupun dengan menggunakan automated toolseperti ProVerif. Protokol coercion-resistance yang diverifikasi adalah protokol milik Stefan G. Weber yang implementasi purwa-rupanya menghasilkan runtime yang linier dengan jumlah vote. Sehingga protokol ini dianggap mampu untuk diimplementasikan di dunia nyata dalam skala pemilihan yang besar. Hasil verifikasi protokol ini membuktikan bahwa protokol tidak dapat memenuhi properti coercion-resistance yang berupa ketahanan terhadap simulation attack, yaitu tidak dimungkinkannya seorang voter menipu coercer dengan cara memberikan rahasia palsu yang dapat digunakan untuk melakukan vote

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.

Kata Kunci : verifikasi protokol, coercion-resistance, applied π-calculus