Election Verifiability Revisited: Automated Security Proofs and Attacks on Helios and Belenios

E-print/Working paper (2020)

Election verifiability aims to ensure that the outcome produced by electronic voting systems correctly reflects the intentions of eligible voters, even in the presence of an adversary that may corrupt ... [more ▼]

Election verifiability aims to ensure that the outcome produced by electronic voting systems correctly reflects the intentions of eligible voters, even in the presence of an adversary that may corrupt various parts of the voting infrastructure. Protecting such systems from manipulation is challenging because of their distributed nature involving voters, election authorities, voting servers and voting platforms. An adversary corrupting any of these can make changes that, individually, would go unnoticed, yet in the end will affect the outcome of the election. It is, therefore, important to rigorously evaluate whether the measures prescribed by election verifiability achieve their goals. We propose a formal framework that allows such an evaluation in a systematic and automated way. We demonstrate its application to the verification of various scenarios in Helios and Belenios, two prominent internet voting systems. For Helios, our analysis is the first one to be, at the same time, fully automated (with the Tamarin protocol prover) and to precisely capture its end-to-end verifiability guarantees, allow- ing us to derive new security proofs and new attacks on deployed versions of it. For Belenios, similarly, we capture precisely the end-to-end verifiability guarantees when all election authorities are corrupted, which is outside the scope of previous formal definitions. We also find new attacks that apply in weaker corruption scenarios that are expected to be secure. In general, our framework allows a unified analy- sis and comparison of cryptographic voting protocols, corruption scenarios and verifiability procedures towards ensuring the end goal of election integrity. [less ▲]

An efficient approach towards the source-target control of Boolean networks

in IEEE/ACM Transactions on Computational Biology and Bioinformatics (2020), 17(6), 1932-1945

We study the problem of computing a minimal subset of nodes of a given asynchronous Boolean network that need to be perturbed in a single-step to drive its dynamics from an initial state to a target ... [more ▼]

We study the problem of computing a minimal subset of nodes of a given asynchronous Boolean network that need to be perturbed in a single-step to drive its dynamics from an initial state to a target steady state (or attractor), which we call the source-target control of Boolean networks. Due to the phenomenon of state-space explosion, a simple global approach that performs computations on the entire network, may not scale well for large networks. We believe that efficient algorithms for such networks must exploit the structure of the networks together with their dynamics. Taking this view, we derive a decomposition-based solution to the minimal source-target control problem which can be significantly faster than the existing approaches on large networks. We then show that the solution can be further optimised if we take into account appropriate information about the source state. We apply our solutions to both real-life biological networks and randomly generated networks, demonstrating the efficiency and efficacy of our approach. [less ▲]

Accelerated verification of parametric protocols with decision trees

in Proceedings of the 38th International Conference on Computer Design (ICCD) (2020)

Proceedings of the 6th International Symposium on Dependable Software Engineering. Theories, Tools, and Applications

Book published by Springer (2020)

Higher-order graph convolutional embedding for temporal networks

in Proceedings of the 21st International Conference on Web Information System Engineering (WISE'20) (2020)

Sequential Temporary and Permanent Control of Boolean Networks.

in Proceedings of the 18th International Conference on Computational Methods in Systems Biology (CMSB) (2020)

Preface (Special section on software systems 2020)

in Journal of Computer Science and Technology (2020), 35(6), 1231-1233

Controlling large Boolean networks with single-step perturbations

in Bioinformatics (2019), 35(14), 558-567

Taming asynchrony for attractor detection in large Boolean networks

in IEEE/ACM Transactions on Computational Biology and Bioinformatics (2019), 16(1), 31-42

Scalable control of asynchronous Boolean networks

in Proceedings of 17th International Conference on Computational Methods in Systems Biology (CMSB'19) (2019)