A Type System for Privacy Properties

Abstract : Mature push button tools have emerged for checking trace properties (e.g. secrecy or authentication) of security protocols. The case of indistinguishability-based privacy properties (e.g. ballot privacy or anonymity) is more complex and constitutes an active research topic with several recent propositions of techniques and tools. We explore a novel approach based on type systems and provide a (sound) type system for proving equivalence of protocols, for a bounded or an unbounded number of sessions. The resulting prototype implementation has been tested on various protocols of the literature. It provides a significant speed-up (by orders of magnitude) compared to tools for a bounded number of sessions and complements in terms of expressiveness other state-of-the-art tools, such as ProVerif and Tamarin: e.g., we show that our analysis technique is the first one to handle a faithful encoding of the Helios e-voting protocol in the context of an untrusted ballot box.
Type de document :
Communication dans un congrès
CCS'17 - 24th ACM Conference on Computer and Communications Security, Oct 2017, Dallas, United States. pp.409 - 423, 2017
Liste complète des métadonnées

Littérature citée [56 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01626109
Contributeur : Véronique Cortier <>
Soumis le : lundi 30 octobre 2017 - 12:31:21
Dernière modification le : jeudi 11 janvier 2018 - 06:27:43
Document(s) archivé(s) le : mercredi 31 janvier 2018 - 12:40:03

Fichier

main-ccs.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01626109, version 1

Citation

Véronique Cortier, Niklas Grimm, Joseph Lallemand, Matteo Maffei. A Type System for Privacy Properties. CCS'17 - 24th ACM Conference on Computer and Communications Security, Oct 2017, Dallas, United States. pp.409 - 423, 2017. 〈hal-01626109〉

Partager

Métriques

Consultations de la notice

278

Téléchargements de fichiers

187