Home // SnT // Research // APSIA // Events // SEQUOIA Annual Meeting - June 2018

SEQUOIA Annual Meeting - June 2018

Belval 11 June 2018

Location: Room MSA 2.400, Maison du Savoir, Belval Campus, University of Luxembourg

Getting there: https://wwwen.uni.lu/contact/belval_campus


10.30 - 11.00: Coffee

11.00 - 11.30: Marie-Laure Zollinger: “Electryo, a Paper-Based Electronic Voting Scheme with Individual Verifiability and Universal (Eligibility) Verifiability”

11.30 - 12.00: Sergiu Bursuc: “Private votes on untrusted platforms”

12.00 - 12.30: Peter Y.A. Ryan (joint work with Bill Roscoe and Geoffroy Couteau): “Stochastic Fair Exchange”

12:30 - 14:00: Lunch

14:00 - 14:30: Antoine Dallon: TBA

14:30 – 15:00: Itsaka Rakotonirina, “The DEEPSEC prover”

15:00 – 15:30: Mathieu Turuani: “A Formal Analysis of the Neuchâtel e-voting protocol”

15:30 – 16:00: Coffee

16:00 – 16:30: Steve Kremer, “An extensive analysis of multi-factor authentication protocols“

16:30 – 17:00: Peter Roenne: “HoneyPAKEs”



Speaker: Mathieu Turuani

Title: A Formal Analysis of the Neuchâtel e-voting protocol


Remote electronic voting is used in several countries for legally binding elections. Unlike academic voting protocols, these systems are not always documented and their security is rarely analysed rigorously.

We study a voting system that has been used for electing political representatives and in citizen-driven referenda in the Swiss canton of Neuchâtel. We design a detailed model of the protocol in ProVerif for both privacy and verifiability properties. Our analysis mostly confirms the security of the underlying protocol: we show that the Neuchâtel protocol guarantees ballot privacy, even against a corrupted server; it also ensures cast-as-intended and recorded-as-cast verifiability, even if the voter’s device is compromised. To our knowledge, this is the first time a full-fledged automatic symbolic analysis of an e-voting system used for politically-binding elections has been realized.


Speaker: Marie-Laure Zollinger, joint work with P. Y. A. Ryan and P. Roenne

Title: Electryo, a Paper-Based Electronic Voting Scheme with Individual Verifiability and Universal (Eligibility) Verifiability

Abstract: Selene is an e-voting protocol that allows voters to directly check their individual vote in the final list of cast votes via a tracker system, while still providing good coercion mitigation. The Selene mechanism can be applied to many e-voting schemes, but here we suggest an application to a polling station scheme providing a paper-based ballot record. The system uses a smartcard-based public key system both to bootstrap the individual verification and to provide universal eligibility verifiability. The paper record contains an encrypted link to the voter’s identity and thus have stronger assumptions on ballot privacy than normal paper voting, but the upside is very good auditability and dispute resolution properties which can be used to create dependable election outcomes in a distrustful setting.


Speaker: Peter Roenne, joint work with J. Lopez-Becerra, P. Y. A. Ryan, P. Sala and M. Skrobot

Title: HoneyPAKEs

Abstract: We combine two security mechanisms: using a Password-based Authenticated Key Establishment (PAKE) protocol to protect the password for access control and the Honeywords construction of Juels and Rivest to detect loss of password files.  The resulting construction combines the properties of both mechanisms: ensuring that the password is intrinsically protected by the PAKE protocol during transmission and the Honeywords mechanisms for detecting attempts to exploit a compromised password file. Our constructions lead very naturally to a two factor type protocols. An enhanced version of our protocol further provides protection against a compromised login server by ensuring that it does not learn the index to the true password.


Speaker: Sergiu Bursuc, joint work with Catalin Dragan and Steve Kremer

Title: Private votes on untrusted platforms

Abstract: We study the problem of guaranteeing vote privacy in the particularly tricky case where the platform used for voting may be corrupted, e.g.

infected by malware. We propose a new definition, formalized as a cryptographic indistinguishability game, evaluate this definition by showing that it captures both known and novel attacks in this setting, and propose a scheme that is provably secure. Furthermore, the corresponding security proof is formalized and machine-checked in EasyCrypt.




Speaker: Itsaka Rakotonirina, Vincent Cheval and Steve Kremer

Title: The DEEPSEC prover

Abstract: Automated verification has become an essential part in the security evaluation of cryptographic protocols. Recently, there has been a considerable effort to lift the theory and tool support that existed for reachability properties to the more complex case of equivalence properties. In this work we contribute both to the theory and practice of this verification problem. We establish new complexity results for static equivalence, trace equivalence and labelled bisimilarity and provide a decision procedure for these equivalences in the case of a bounded number of sessions. We implemented the procedure in a new tool, DEEPSEC. We showed through extensive experiments that it is significantly more efficient than other similar tools, while at the same time raises the scope of the protocols that can be analysed.



Speaker: Steve Kremer, Charlie Jacomme

Title: An extensive analysis of multi-factor authentication protocols

Abstract: Passwords are still the most widespread means for authenticating users, even though they have been shown to create huge security problems. This motivated the use of additional authentication mechanisms used in so-called multi-factor authentication protocols. In this paper we define a detailed threat model for this kind of protocols: while in classical protocol analysis attackers control the communication network, we take into account that many communications are performed over TLS channels, that computers may be infected by different kinds of malwares, that attackers could perform phishing, and that humans may omit some actions.

We formalize this model in the applied pi calculus and perform an extensive analysis and comparison of several widely used protocols - variants of Google 2-step and FIDO’s U2F. The analysis is completely automated, generating systematically all combinations of threat scenarios for each of the protocols and using the Proverif tool for automated protocol analysis. Our analysis highlights weaknesses and strengths of the different protocols, and allows us to suggest several small modifications of the existing protocols which are easy to implement, yet improve their security in several threat scenarios.