Home

People

Papers & Software

Seminar

Stages



INRIA

LIX

CNRS
Propositions de theses 2007

Available stages' subjects:

Reasoning about information-hiding protocols

Encadrement :

Catuscia Palamidessi, INRIA-Futurs and LIX.

Keywords

Privacy, Anonymity, Information Theory, Statistical inference, Epistemic Logic.

Description

The increasing diffusion of electronic services is accompanied by an increasing concern for the protection of private information. There is therefore a growing interest in the design of protocols to ensure properties like anonymity, privacy, and secrecy, as well as in the study of the formal aspects of such properties and in the development of proper tools for ensuring the correctness of these protocols. Many of these protocols use randomization to conceal the correlation between the information to be hidden and the observable events. Attackers, on the other hand, may use statistical analysis to try to infer the secret information from the observables.

Goal

In this proposal, we aim at establishing a formal framework for expressing and reasoning about information-hiding properties, for helping the design of adequate protocols, and for verifying them. In order to cope with the aspects of randomization and statistical inference, we plan to use a probabilistic approach. In particular, we plan to use Information Theory. We believe that the body of concepts and results related to the notion of entropy will provide a natural and solid framework for our goals. We also plan to apply notions from statistical inference, like the Bayesian decision functions and the associated probability of error. Finally, we aim at developing a probabilistic epistemic logic for reasoning about information-hiding properties.

Related projects

This thesis proposal is related to the INRIA/DREI project Printemps

Bibliography

Some preliminary ideas (restricted to the case of anonymity) are described in the papers

  1. Mohit Bhargava, Catuscia Palamidessi Probabilistic Anonymity. Proc. of CONCUR 2005, pages 171-185 [pdf]
  2. Kostas Chatzikokolakis, Catuscia Palamidessi, Prakash Panangaden. Anonymity Protocols as Noisy Channels. Postproc. of TGC'06, LNCS, Springer. To appear [pdf]

Process Calculi for Security

Encadrement :

Frank Valencia, CNRS and LIX, and
Catuscia Palamidessi, INRIA-Futurs and LIX.

Description du sujet

Process calculi are being used to find potential attacks in security protocols. Most modern calculi for security are based on a monotonic shared-memory model. The idea is that the agents of the protocol interact by communicating through a shared store where items of information (encrypted or not) reside. The monotonicity of the store (i.e., messages cannot be removed from the store) models the fact that once a message is sent, it becomes available to every one on the network; in particular to malicious agents. Typically, these calculi are also parametric in a logic to reason about what can be inferred from the information in the store. The inferred information may then reveal a flaw in the protocol. The work in process calculi for security is  under development;  more theories and reasoning techniques are needed.

Now, CCP (Concurrent Constraint Programming) is a well-established and mature model for concurrency with several reasoning techniques and strong ties to logic---- CCP agents can alternatively be viewed as logic formulae, algebraic terms and computational processes. Now, similarly the the above calculi, CCP is based on a monotonic shared-memory model and parametric in an information system. Process interact by communication through the shared store and the underlying information systems is used to reason about what can be inferred from the shared information.

Goal

The goal of this thesis is to explore the use of CCP theory to enrich that of process calculi for security as well to generalize CCP to reason about security.

Bibliography

  1. Martín Abadi, Andrew D. Gordon. A Calculus for Cryptographic Protocols: The Spi Calculus. Information and Computation, 148(1), pp. 1-70, 1999. [ps of report version].

  2. Michele Boreale, Marzia Buscemi. A Framework for the Analysis of Security Protocol. In Proc. of CONCUR '02, LNCS 2421, Springer-Verlag, 2002. [ps]

  3. F. Crazzolara and G. Winskel. Events in Security Protocols. In Proc. of the ACM Conference on Computer and Communications Security. 2001. [pdf]

  4. R. Amadio, D. Lugiez and V. Vanackère. On the Symbolic Reduction of Processes with Cryptographic Functions. Theoretical Computer Science, Vol 290. 2003. [pdf]

  5. V. Saraswat, M. Rinard and P. Panagaden. Semantic foundations for concurrent constraint programming. In Proc. of the ACM Symposium on Principles of Programming Languages. 1991. [pdf]


Page maintainer: Catuscia Palamidessi