349
views
0
recommends
+1 Recommend
1 collections
    4
    shares
      • Record: found
      • Abstract: found
      • Conference Proceedings: found
      Is Open Access

      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) (VECOS)

      Verification and Evaluation of Computer and Communication Systems (VECoS 2010)

      1-2 July 2010

      Electronic-voting protocols, Formal verification, mCRL2, Eligibility, Uniqueness

      Read this article at

      Bookmark
          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

          Abstract

          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.

          Related collections

          Most cited references 1

          • Record: found
          • Abstract: not found
          • Article: not found

          A framework and taxonomy for comparison of electronic voting schemes

            Bookmark

            Author and article information

            Contributors
            Conference
            July 2010
            July 2010
            : 1-9
            Affiliations
            Network Security Center

            Department of Computer Engineering

            Sharif University of Technology

            Tehran, Iran
            Article
            10.14236/ewic/VECOS2010.10
            © Hamid Reza Mahrooghi et al. Published by BCS Learning and Development Ltd. Fourth International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2010), Paris, France

            This work is licensed under a Creative Commons Attribution 4.0 Unported License. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/

            Fourth International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2010)
            VECOS
            4
            Paris, France
            1-2 July 2010
            Electronic Workshops in Computing (eWiC)
            Verification and Evaluation of Computer and Communication Systems (VECoS 2010)
            Product
            Product Information: 1477-9358BCS Learning & Development
            Self URI (journal page): https://ewic.bcs.org/
            Categories
            Electronic Workshops in Computing

            Comments

            Comment on this article