電子投票プロトコルに対する無証拠性の定理証明  [in Japanese] Theorem-proving Receipt-freeness of an e-voting Protocol  [in Japanese]

電子投票プロトコルの満たすべき性質に,無証拠性があげられる.これは匿名性の拡張で,「プロトコルを観測して得られる情報に加えて,別の付加的な情報を投票者が外部に与えたとしても,ある投票パターンと別の(結果が同じとなる)投票パターンが区別できない」という性質である.本稿では,Leeらの電子投票プロトコルを題材とし,その無証拠性を定理証明器で形式的に検証する.

Receipt-freeness is an important property for an e-voting protocol. This is an extension of anonymity and means that two voting patterns with the same result cannot be distinguishable, even if the voter supplies additional information outside the scope of the protocol. In this paper, we deal with an e-voting protocol by Lee, et al., and we theorem-prove the receipt-freeness of the protocol formally.