Text size
  • Small
  • Medium
  • Large
  • Standard
  • Blue text on blue
  • High contrast (Yellow text on black)
  • Blue text on beige

    Formal Verification of Authentication-Type Properties of an Electronic Voting Protocol Using mCRL2

    Fourth International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2010)

    Paris, France, 1 - 2 July 2010


    Hamid Reza Mahrooghi, Mohammad Hashem Haghighat and Rasool Jalili


    Having a doubtless election in the information technology era requires satisfaction and verification of security properties in electronic voting (e-voting) systems. This paper focuses on verification of authentication-type properties of an e-voting protocol. The well-known FOO92 e-voting protocol is analyzed, as a case study, against the uniqueness and eligibility properties and their satisfaction are verified. By means of an automated formal approach, the protocol is modelled in the mCRL2 language, which is a combination of the ACP process algebra language and abstract data types (ADT). Then, the eligibility and uniqueness properties as two authentication-type requirements are modelled in the modal μ-calculus. These are given to a combination of dedicated mCRL2 tools to verify the properties. Our research is valuable due to its direct modelling of authentication-type properties and their verification. The experiment can be easily generalized as a pattern for verification of similar protocols.


    PDF filePDF Version of this Paper (278kb)