-
A Type System for Privacy Properties (Technical Report)
Authors:
Véronique Cortier,
Niklas Grimm,
Joseph Lallemand,
Matteo Maffei
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 (sou…
▽ More
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.
△ Less
Submitted 28 August, 2017;
originally announced August 2017.
-
Proceedings 8th International Workshop on Security Issues in Concurrency
Authors:
Konstantinos Chatzikokolakis,
Véronique Cortier
Abstract:
This volume contains the proceedings of the 8th Workshop on Security Issues in Concurrency (SecCo 2010). The workshop was held in Paris, France on August 30th, 2010, as a satellite workshop of CONCUR'10. The aim of the SecCo workshop series is to cover the gap between the security and the concurrency communities. More precisely, the workshop promotes the exchange of ideas, trying to focus on commo…
▽ More
This volume contains the proceedings of the 8th Workshop on Security Issues in Concurrency (SecCo 2010). The workshop was held in Paris, France on August 30th, 2010, as a satellite workshop of CONCUR'10. The aim of the SecCo workshop series is to cover the gap between the security and the concurrency communities. More precisely, the workshop promotes the exchange of ideas, trying to focus on common interests and stimulating discussions on central research questions. In particular, we called for papers dealing with security issues (such as authentication, integrity, privacy, confidentiality, access control, denial of service, service availability, safety aspects, fault tolerance, trust, language-based security, probabilistic and information theoretic models) in emerging fields like web services, mobile ad-hoc networks, agent-based infrastructures, peer-to-peer systems, context-aware computing, global/ubiquitous/pervasive computing.
△ Less
Submitted 25 February, 2011;
originally announced February 2011.
-
YAPA: A generic tool for computing intruder knowledge
Authors:
Mathieu Baudet,
Véronique Cortier,
Stéphanie Delaune
Abstract:
Reasoning about the knowledge of an attacker is a necessary step in many formal analyses of security protocols. In the framework of the applied pi calculus, as in similar languages based on equational logics, knowledge is typically expressed by two relations: deducibility and static equivalence. Several decision procedures have been proposed for these relations under a variety of equational theori…
▽ More
Reasoning about the knowledge of an attacker is a necessary step in many formal analyses of security protocols. In the framework of the applied pi calculus, as in similar languages based on equational logics, knowledge is typically expressed by two relations: deducibility and static equivalence. Several decision procedures have been proposed for these relations under a variety of equational theories. However, each theory has its particular algorithm, and none has been implemented so far. We provide a generic procedure for deducibility and static equivalence that takes as input any convergent rewrite system. We show that our algorithm covers most of the existing decision procedures for convergent theories. We also provide an efficient implementation, and compare it briefly with the tools ProVerif and KiSs.
△ Less
Submitted 5 May, 2010;
originally announced May 2010.
-
Deciding security properties for cryptographic protocols. Application to key cycles
Authors:
Hubert Comon-Lundh,
Véronique Cortier,
Eugen Zalinescu
Abstract:
There is a large amount of work dedicated to the formal verification of security protocols. In this paper, we revisit and extend the NP-complete decision procedure for a bounded number of sessions. We use a, now standard, deducibility constraints formalism for modeling security protocols. Our first contribution is to give a simple set of constraint simplification rules, that allows to reduce any…
▽ More
There is a large amount of work dedicated to the formal verification of security protocols. In this paper, we revisit and extend the NP-complete decision procedure for a bounded number of sessions. We use a, now standard, deducibility constraints formalism for modeling security protocols. Our first contribution is to give a simple set of constraint simplification rules, that allows to reduce any deducibility constraint system to a set of solved forms, representing all solutions (within the bound on sessions).
As a consequence, we prove that deciding the existence of key cycles is NP-complete for a bounded number of sessions. The problem of key-cycles has been put forward by recent works relating computational and symbolic models. The so-called soundness of the symbolic model requires indeed that no key cycle (e.g., enc(k,k)) ever occurs in the execution of the protocol. Otherwise, stronger security assumptions (such as KDM-security) are required.
We show that our decision procedure can also be applied to prove again the decidability of authentication-like properties and the decidability of a significant fragment of protocols with timestamps.
△ Less
Submitted 20 March, 2009; v1 submitted 27 August, 2007;
originally announced August 2007.
-
Relating two standard notions of secrecy
Authors:
Veronique Cortier,
Michael Rusinovitch,
Eugen Zalinescu
Abstract:
Two styles of definitions are usually considered to express that a security protocol preserves the confidentiality of a data s. Reachability-based secrecy means that s should never be disclosed while equivalence-based secrecy states that two executions of a protocol with distinct instances for s should be indistinguishable to an attacker. Although the second formulation ensures a higher level of…
▽ More
Two styles of definitions are usually considered to express that a security protocol preserves the confidentiality of a data s. Reachability-based secrecy means that s should never be disclosed while equivalence-based secrecy states that two executions of a protocol with distinct instances for s should be indistinguishable to an attacker. Although the second formulation ensures a higher level of security and is closer to cryptographic notions of secrecy, decidability results and automatic tools have mainly focused on the first definition so far.
This paper initiates a systematic investigation of the situations where syntactic secrecy entails strong secrecy. We show that in the passive case, reachability-based secrecy actually implies equivalence-based secrecy for digital signatures, symmetric and asymmetric encryption provided that the primitives are probabilistic. For active adversaries, we provide sufficient (and rather tight) conditions on the protocol for this implication to hold.
△ Less
Submitted 6 July, 2007; v1 submitted 4 June, 2007;
originally announced June 2007.
-
Explicit Randomness is not Necessary when Modeling Probabilistic Encryption
Authors:
Véronique Cortier,
Heinrich Hördegen,
Bogdan Warinschi
Abstract:
Although good encryption functions are probabilistic, most symbolic models do not capture this aspect explicitly. A typical solution, recently used to prove the soundness of such models with respect to computational ones, is to explicitly represent the dependency of ciphertexts on random coins as labels. In order to make these label-based models useful, it seems natural to try to extend the unde…
▽ More
Although good encryption functions are probabilistic, most symbolic models do not capture this aspect explicitly. A typical solution, recently used to prove the soundness of such models with respect to computational ones, is to explicitly represent the dependency of ciphertexts on random coins as labels. In order to make these label-based models useful, it seems natural to try to extend the underlying decision procedures and the implementation of existing tools. In this paper we put forth a more practical alternative based on the following soundness theorem. We prove that for a large class of security properties (that includes rather standard formulations for secrecy and authenticity properties), security of protocols in the simpler model implies security in the label-based model. Combined with the soundness result of (\textbf{?}) our theorem enables the translation of security results in unlabeled symbolic models to computational security.
△ Less
Submitted 7 June, 2006;
originally announced June 2006.
