A Type System for Privacy Properties

被引:14
作者
Cortier, Veronique [1 ]
Grimm, Niklas [2 ]
Lallemand, Joseph [3 ]
Maffei, Matteo [2 ]
机构
[1] CNRS, LORIA, Nancy, France
[2] TU Wien, Vienna, Austria
[3] INRIA, LORIA, Nancy, France
来源
CCS'17: PROCEEDINGS OF THE 2017 ACM SIGSAC CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY | 2017年
基金
欧洲研究理事会;
关键词
Protocols; privacy; symbolic models; type systems; VERIFICATION; TOOL;
D O I
10.1145/3133956.3133998
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
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.
引用
收藏
页码:409 / 423
页数:15
相关论文
共 51 条
  • [1] Private authentication
    Abadi, M
    Fournet, C
    [J]. THEORETICAL COMPUTER SCIENCE, 2004, 322 (03) : 427 - 476
  • [2] Abadi M, 2000, NATO ADV SCI I F-COM, V175, P39
  • [3] Mobile values, new names, and secure communication
    Abadi, M
    Fournet, C
    [J]. ACM SIGPLAN NOTICES, 2001, 36 (03) : 104 - 115
  • [4] Abadi Martin., 2000, Proceedings of the IFIP International Conference on Theoretical Computer Science, P3, DOI [10.1007/3-540-44929-9_1, DOI 10.1007/3-540-44929-9_1]
  • [5] Adida B., 2008, USENIX, P335
  • [6] [Anonymous], 2014, Lecture Notes in Computer Science
  • [7] Antonopoulos T, 2017, ACM SIGPLAN NOTICES, V52, P362, DOI [10.1145/3140587.3062378, 10.1145/3062341.3062378]
  • [8] Arapinis M., 2009, P ICITST, P1
  • [9] When Are Three Voters Enough for Privacy Properties?
    Arapinis, Myrto
    Cortier, Veronique
    Kremer, Steve
    [J]. COMPUTER SECURITY - ESORICS 2016, PT II, 2016, 9879 : 241 - 260
  • [10] Analysing Unlinkability and Anonymity Using the Applied Pi Calculus
    Arapinis, Myrto
    Chothia, Tom
    Ritter, Eike
    Ryan, Mark
    [J]. 2010 23RD IEEE COMPUTER SECURITY FOUNDATIONS SYMPOSIUM (CSF), 2010, : 107 - 121