 |
|
|
|
| Propositions de stage 2011 |
|
Available stages' subjects:
- Stages on the subject "Protection of Private Information"
- Stage on the subject "A Spatial Concurrent-Constraint Calculus"
- Stage on the subject "A Process Calculus for Epistemic Reasoning"
Some success stories
Comète PhD student wins the prize Specif / Gilles Kahn for 2008
Protection of Private Information
Encadrement :
Catuscia Palamidessi, INRIA-Futurs and LIX.Background
The increasing diffusion of electronic services and of the use of the internet makes it possible to collect, store and exchange increasingly large amount of information about the user. This may include confidential data like the identity of the user, his contact information, his preferences as a consumer, etc. It is often the case that this privacy intrusion is done without the consent of the user, and in the worst case the user may not even be aware of it. Protocols to ensure protection of confidential information are therefore in high demand, and their design and foundations are a very active topic of research. Many of these protocols use randomization to obfuscate the link between the public information and the information that has to be kept secret.
We have various stages available as part of a general project which aims at establishing the foundations of a framework for information protection. Part of the effort will be devoted to the formalization of protection properties: In fact, these properties are not well understood yet, especially in presence of randomization. The ultimate goal is the synthesis of automatic tools for verifying that a protocol satisfies the intended degree of protection. Our approach is to use a probabilistic process calculus to specify the protocols, to develop the theoretical foundations of quantitative information leakage, and a model checker for the calculus able to verify efficiently that a protocol satisfies the desired degree of protection.
Stages available
1) Persistent Adversaries
The adversary may be able to enforce the re-execution of the protocol several times, thus increasing his collection of public data (the observables). Intuitively, this will increase his capability of inferring information about the secret data. In [CPP-JCS] we have studied the case in which the adversary is able to enforce that the secret remains the same trough the re-executions, which is naturally related to the inference of the secret. Preliminary studies show that, in case the adversary wants to infer the distribution on the secrets, then the best strategy is to let the secret change trough the re-executions. In this stage proposal we intend to study (a) the techniques that a persistent adversary can use to infer the distribution, and (b) the conditions which make the protocol robust wrt the attacks of this kind of persistent adversary.2) Interactive Adversaries
An interactive adversary may be able to interfere with the execution of the protocol, and even influence the behavior of the users, to a certain extent. While in a presence of a passive adversary the protocol can be modeled by an information-theoretic channel [CPP-IC], this is not anymore the case when the adversary is interactive. In this stage proposal, we intend to study the model that such a kind of adversary leads to, and extend the notion of protection proposed in [CPP-IC] to cope with this kind of adversary.3) The Problem of the Scheduler
The problem of the scheduler can be illustrated via an example on the Dining Cryptographers (see, for instance, [CP-IC]). Assume that a scheduler always schedules last for the output declaration the cryptographer who pays. Then the protocol will not provide any protection of the identity of the payer (anonymity), because an observer who knows the behavior of the scheduler can infer with certainty who is the payer. This scenario is quite realistic, since we can imagine that the payer has a heavier working load, and the scheduler gives priority to lighter processes. This problem is encountered in [BCP-FOSSACS]: In that paper we have studied a characterization of safe constructs, namely constructs in a probabilistic process calculus that, whenever applied to a term (representing a protocol), do not decrease its degree of protection. The fact that the scheduler may leak secrets restricts dramatically the class of safe constructs. In this stage proposal, we aim at defining constraints on the scheduler so to avoid the problem of the information leakage, and extend the results of [BCP-FOSSACS] to a more general class of constructs.4) Information Leakage and Hypothesis Testing
We propose a method to analyse the information leakage based on hypothesis testing. The two main rules adopted in this setting are the Maximum Aposteriori Probability and the Maximum Likelihood [CPP-JCS,CPP-IC]. We aim at defining a new rule, based on the notion of distance between distributions, with the aim of combining the advantages of the two.Continuation
It will be possible to continue the work described in the stage proposals as a PhD student.Bibliography
[CPP-JCS] K. Chatzikokolakis, C. Palamidessi, P. Panangaden. On the Bayes Risk in Information-Hiding Protocols. Journal of Computer Security, 16(5):531-571, 2008. [Report version].
[CPP-IC] K. Chatzikokolakis, C. Palamidessi, P. Panangaden. Anonymity Protocols as Noisy Channels. Information and Computation, 206(2-4):378-401, 2008. [Report version].
[CP-IC] K. Chatzikokolakis, C. Palamidessi. Making Random Choices Invisible to the Scheduler. Information and Computation. To appear. [Report version ]
[BCP-FOSSACS] C. Braun, K. Chatzikokolakis, C. Palamidessi. Compositional Methods for Information-Hiding. Proceedings of FOSSACS 2008, LNCS 4962, Springer, 443-457, 2008. [Report version].
A Spatial Concurrent-Constraint Calculus
Encadrement :
Frank D. Valencia, CNRS and LIX.Description du sujet
The Ambients process calculus [SCCP-SC] is a formalism to model the behavior and structure of mobile systems. Spatial logics [SCCP-SL] are formalisms that can be used to specify properties these systems must comply with. For example that the system must be composed of several identifiable subsystems possibly including hierarchies of named locations restricting the use of certain resources to certain subsystems.
The process calculus CCP (Concurrent Constraint Programming) [SCCP-CCP] is a well-established formalism for concurrency for reasoning about agents which interact with each other by telling and asking information represented as logic formulae also known as constraints (e.g., x > 42). This calculus is parametric in a constraint system which is basically an underlying logic theory. A distinctive feature of CCP is that agents can be viewed as both processes and formulae in the underlying logic.
The purpose of this stage is to use CCP to reason about the behavior and structure of mobile systems as those modelled in Ambients. The approach involves using a spatial logic as the underlying constraint system. It may also involve tailoring CCP to deal with typical process constructions of the Ambients calculus. Following the tradition of CCP, we aim at one single formalism where Spatial CCP agents can be seen as both processes and spatial logic formulae.
It will be possible to continue this work as a PhD student.
Bibliography
[SCCP-SL] L. Caires and L. Cardelli. A Spatial Logic for Concurrency (Part I). Journal of Information and Computation. 186(2), 2003, Elsevier. [Authors' online version].
[SCCP-CCP] V. Saraswat, M. Rinard, P. Panangaden. Semantic Foundations of Concurrent Constraint Programming. POPL 1991. 333-352, ACM. [Citeseer online version].
[SCCP-SC] L. Cardelli. Mobile Ambients Theoretical Computer Science, Special Issue on Coordination. Vol 240/1, pp 177-213. 2000. [Author's online version].
A Process Calculus for Epistemic Reasoning
Encadrement :
Frank D. Valencia, CNRS and LIX.Description du sujet
Epistemic logic is a formalism to reason about knowledge and belief [1]. It has been used and adapted for diverse areas of computer science to derive properties of multi-agent systems that involve issues such as common and distributed knowledge, explicit and implicit belief, and the interplay between knowledge and time. Particularly interesting applications can be found in the realm of Security Protocols where agents are meant to exchange information and verify properties such as secrecy and anonymity [2].
The process calculus CCP (Concurrent Constraint Programming) [3] is a well-established formalism from Concurrency Theory for reasoning about agents that interact with each other by telling and asking information represented as logic formulae (also known as constraints). This calculus is parametric in a constraint system which is basically an underlying logic theory. A distinctive feature of CCP is that agents can be viewed as both processes and formulae in the underlying logic. It also provides several verification techniques focused on reachability analysis. Information exchange and reachability analysis are fundamental for security analysis (e.g., to show that a system may reach a state where a secret is revealed to a malicious agent). Consequently, CCP has also been shown to be suitable for modelling Security Protocols [4].
The purpose of this stage is to use CCP to reason about agents interacting with epistemic knowledge. The approach involves using an epistemic logic as the underlying constraint system. It may also involve tailoring CCP to deal with typical constructions from this logic. Following the tradition of CCP, we aim at one single formalism where agents can be seen as both processes and epistemic logic formulae.
It will be possible to continue this work as a PhD student. The PhD work will involve the development of reasoning and verification techniques to predict the outcomes of the encoded systems. In particular, we expect this new approach to bring new insights into the verification of Security Protocols using CCP.
Bibliography
[1] Jaakko Hintikka. Knowledge and Belief: An Introduction to the Logic of the Two Notions. Cornell University Press, Ithaca, N. Y., 1962.
[2] Rohit Chadha, Stéphanie Delaune, Steve Kremer: Epistemic Logic for the Applied Pi Calculus.FMOODS/FORTE 2009: 182-197. [Author's online version].
[3] V. Saraswat, M. Rinard, P. Panangaden. Semantic Foundations of Concurrent Constraint Programming. POPL 1991. 333-352, ACM. [Citeseer online version].
[4] C. Olarte and F. Valencia. The Expressivity of Universal Timed CCP: Undecidability of Monadic FLTL and Closure Operators for Security. PPDP'08: 8-19. ©ACM Press. 2008. [Author's online version].
Some success stories
PhD price Specif / Gilles Kahn Konstantinos Chatzikokolakis, ancien stagiaire and PhD student in Comète under the direction of Catuscia Palamidessi, has won one of the two second prices Specif / Gilles Kahn in 2008 for his PhD thesis.
Below we list other recent stages which have been particularly successful. In most of the cases the stagiaire has continued his investigation as a PhD student in our equipe.
- Subject of the stage : Bounds on the leakage of the input's distribution in information-hiding protocols.
Stagiaire: Abhishek Bhowmick (IIT Kanpur, India)
Supervisor: Catuscia Palamidessi Period of the stage: Spring-Summer 2008
Dissemination: The results of this stage have been published in the proceedings of TGC 2008. The report version is available here. - Subject of the stage : Compositional Methods for Information-Hiding.
Stagiaire: Christelle Braun (Ecole de Mines, Computational Logic Master, Dresden)
Supervisor: Catuscia Palamidessi Period of the stage: Spring-Summer 2007
Dissemination: The results of this stage have been published in the proceedings of FOSSACS 2008. The report version is available here. - Subject of the stage : On the Asynchronous Nature of the Asynchronous pi-Calculus.
Stagiaire: Romain Beauxis (Ecole Centrale, Paris)
Supervisor: Catuscia Palamidessi Period of the stage: Fall 2006
Dissemination: The results of this stage have been published in the book Concurrency, Graphs and models. The paper is here. - Subject of the stage : Expressiveness of probabilistic π-calculi.
Stagiaire: Sylvain Pradalier (MPRI, ENS Cachan)
Supervisor: Catuscia Palamidessi Period of the stage: Spring-Summer 2005
Dissemination: The results of this stage have been published in the proceedings of QAPL 2006. The report version is available here. - Subject of the stage : A Framework for Probabilistic Security Protocols.
Stagiaire: Kostas Chatzikokolakis (DEA Programmation, Paris)
Supervisor: Catuscia Palamidessi Period of the stage: Spring-Summer 2004
Dissemination: The results of this stage have been published in the proceedings of TGC 2005. The full version of this paper is accepted for publication in Theoretical Computer Science. The report version is available here. - Subject of the stage : Probabilistic and Nondeterministic Aspects of Anonymity Protocols.
Stagiaire: Mohit Bhargava (IIT New Delhi, India)
Supervisor: Catuscia Palamidessi Period of the stage: Summer 2004
Dissemination: The results of this stage have been published in the proceedings of CONCUR 2005. The full version of this paper is submitted for publication in Theoretical Computer Science. The report version is available here. - Subject of the stage : Probabilistic and Nondeterministic Aspects of Anonymity Protocols.
Stagiaire: Axelle Ziegler (DEA Programmation, Paris)
Supervisor: Dale Miller and Catuscia Palamidessi Period of the stage: Spring-Summer 2004
Dissemination: The results of this stage have been published in the proceedings of SOS 2005. We are preparing the journal version of this paper. The report version is available here.
Page maintainer: Catuscia Palamidessi