Skip to Main content Skip to Navigation

Formal verification of advanced families of security protocols : E-voting and APIs

Abstract : Formal methods have been used to analyze security protocols and several tools have even been developed to tackle automatically different proof techniques and ease the verification of such protocols. However, for electronic voting and APIs, current tools tend to reach their limits because they can’t handle some cryptographic primitives, or the security properties, involved in those protocols. We work on two cases studies of existing and deployed systems: a Norwegian e-voting protocol and a CNRS boardroom voting protocol. We analyze them using the applied pi-calculus model and we discuss in details about their security properties, in different corruption scenarios. Even including several reusable results, these proofs are complex and, therefore, expose a real need for automation. Thus, we focus on a possible lead in direction of this needed automation: type-systems. We build upon a recent work describing a new type-system designed to deal with equivalence properties, in order to apply this on the verification of equivalence-based properties in electronic voting like ballot-secrecy. We present an application of this method through Helios, a well-known e-voting system. Another family of advanced security protocols are APIs: secure interfaces devoted to allow access to some information stored into a secured trusted hardware without leaking it outside. Recet work seems to show that these interfaces are also vulnerable. In this thesis, we provide a new design for APIs, including revocation. In addition, we include a formal analysis of this API showing that a malicious combination of API’s commands does not leak any key, even when the adversary may brute-force some of them
Document type :
Complete list of metadata

Cited literature [102 references]  Display  Hide  Download
Contributor : Thèses UL Connect in order to contact the contributor
Submitted on : Thursday, March 29, 2018 - 1:07:59 PM
Last modification on : Saturday, October 16, 2021 - 11:26:08 AM


Files produced by the author(s)


  • HAL Id : tel-01751142, version 1



Cyrille Wiedling. Formal verification of advanced families of security protocols : E-voting and APIs. Other [cs.OH]. Université de Lorraine, 2014. English. ⟨NNT : 2014LORR0199⟩. ⟨tel-01751142⟩



Record views


Files downloads