FOO e-Voting Protocol: Inductive Analysis of the Eligibility Property

There are two main approaches in verifying security protocols: model checking and theorem proving. Inductive Method is one of the notable works based on pure theorem proving. Although there is no automatic tool to implement this method, it has been successful in analyzing many classic to real world protocols such as SET under an unlimited number of agents interleaving an infinite number of sessions. E-voting protocols are one of the challenging protocols that use different advanced security primitives and should guarantee various complicated security goals. Using the great potential of the Inductive Method in formalizing new concepts, we found the opportunity of analyzing these protocols by this method. We first extend the method to support two common security primitives ( blind signature and bit commitment) used in some e-voting protocols such as FOO'92. Then we show that our extension is compatible with already defined elements of the Inductive Method and it also meets the desired requirements and behaviors. Using our formalizations, we model the e-voting protocol FOO'92. Moreover we specify the eligibility goal and prove by inductive analyses that the protocol guarantees this goal.