Automatic checking of eligibility in electronic voting protocolsusing mCRL2

Eligibility is one of the important security properties which must be satisfied in electronic voting systems. This property refers to legitimacy of voters and their right to vote only once. Due to insufficiency of an observational analysis to guarantee this property, formal methods are recently used to build trust on sensitive systems such as e-voting for all the involved parties. This paper reports our attempt to automatically check the eligibility property in electronic voting systems using the model checking approach. ThemCRL2 language and its toolset are also used to achieve such a checking. Two protocols, FOO92 and Lee&Kim, are modeled as case studies.