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 :
Theses
Complete list of metadatas

Cited literature [102 references]  Display  Hide  Download

https://hal.univ-lorraine.fr/tel-01751142
Contributor : Thèses Ul <>
Submitted on : Thursday, March 29, 2018 - 1:07:59 PM
Last modification on : Tuesday, April 24, 2018 - 1:30:05 PM

File

DDOC_T_2014_0199_WIEDLING.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : tel-01751142, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

78

Files downloads

48