Applying a Dependency Mechanism for Voting Protocol Models Using Event-B

The design of e-voting systems requires the use of techniques which guarantee that the resulting system is safe, secure and preserves privacy. We develop Event-B models of a voting system, by applying a decomposition pattern and a technique of contextualisation, using a dependency mechanism. Through refinement, we take into account the precise regulation and structure of a specific voting process, and reason formally about the system’s resistence to common attacks and threats.

• Publication year

  2017

• Venue

  Formal Techniques for (Networked and) Distributed Systems

• Publication date

  2017-06-19

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1007/978-3-319-60225-7_9
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Towards an integrated formal method for verification of liveness properties in distributed systems: with application to population protocols

  2017cited by this paper
• A review of E-voting: the past, present and future

  2016cited by this paper
• Towards an integrated formal method for verification of liveness properties in distributed systems: with application to population protocols

  2015cited by this paper
• A generic construction for voting correctness at minimum cost - Application to Helios

  2013cited by this paper
• Modeling Contexts with Dependent Types

  2010cited by this paper
• Modeling in event-b - system and software engineering by Jean-Raymond Abrial

  2010cited by this paper
• Proof-Based Design of Security Protocols

  2010cited by this paper
• Trust and security in the e-voting system

  2009cited by this paper
• Event-B patterns and their tool support

  2009cited by this paper
• Feature Interactions in a Software Product Line for E-voting

  2009cited by this paper
• Modelling Attacker's Knowledge for Cascade Cryptographic Protocols

  2008cited by this paper
• Roadmap for enhanced languages and methods to aid verification

  2006cited by this paper
• Software Engineering 3 - Domains, Requirements, and Software Design

  2006cited by this paper
• Threat Modeling as a Basis for Security Requirements

  2005cited by this paper
• Analysis of an Electronic Voting Protocol in the Applied Pi Calculus

  2005cited by this paper
• Requirements Engineering: Processes and Techniques

  1998cited by this paper
• The temporal logic of actions

  1994cited by this paper
• Notes on Formalizing Context

  1993cited by this paper
• On Conditionals: CONDITIONALS AND CONDITIONAL INFORMATION

  1986cited by this paper

• Verifying System-Level Security of a Smart Ballot Box

  2021cites this paper
• Modelling an E-Voting Domain for the Formal Development of a Software Product Line: When the Implicit Should Be Made Explicit

  2020cites this paper
• Contextual Dependency in State-Based Modelling

  2020cites this paper
• Un cadre formel pour l'intégration de connaissances du domaine dans la conception des systèmes: application au formalisme Event-B. (A formal framework to integrate domain knowledge into system design: Application to Event-B formalism)

  2018cites this paper
• On the Importance of Explicit Domain Modelling in Refinement-Based Modelling Design. Experiments with Event-B

  2018cites this paper
• Formalising the Requirements of an E-Voting Software Product Line Using Event-B

  2018cites this paper
• Contextualization and Dependency in State-Based Modelling - Application to Event-B

  2017cites this paper