Direction des Relations Européennes et Internationales (DREI)
|Projet INRIA : Comète||Organisme étranger partenaire : Mc. Gill University|
|Unité de recherche INRIA : Futurs
Thème INRIA : Systèmes Communicants
|Pays : Canada|
|Nom, prénom||Palamidessi, Catuscia||Panangaden, Prakash|
|Organisme d'appartenance||INRIA||McGill University, School of Computer Science|
|Adresse postale||LIX, École Polytechnique, rue de Saclay, 91128 Palaiseau FRANCE||3480 rue University, Suite 318 Montreal, Quebec H3A 2A7 CANADA|
|Téléphone||+33 (0)1 69 33 37 98||+1 514 3987074|
|Télécopie||+33 (0)1 69 33 30 14||+1 514 3983883|
|Courriel||catuscia at email@example.com|
Titre de la thématique de collaboration :
Probabilité et Théorie de l'Information
pour la protection de l'Anonymat et de l'Information Privée. PRINTEMPS: PRobability and INformation ThEory for
Modeling anonymity, Privacy, and Secrecy
Probabilité et Théorie de l'Information pour la protection de l'Anonymat et de l'Information Privée.
PRINTEMPS: PRobability and INformation ThEory for Modeling anonymity, Privacy, and Secrecy
The increasing diffusion of electronic services is accompanied by an increasing concern for the protection of private information. The design of protocols to ensure properties like anonymity, privacy, and secrecy, is therefore a very active topic of research, as well as the study of the formal aspects of such properties and the development of proper tools for ensuring the correctness of these protocols. However, despite the fact that much research has been done already, almost all the existing theories and verification techniques are along the lines of the so-called possibilistic approach, which is based on the principle of representing as nondeterministic the random mechanisms used in most of this class of protocols.
The nondeterministic approximation however makes it impossible to capture the leakage of probabilistic information and prevent possible attacks based, for instance, on statistical analysis. For this reason, we feel that the theoretical foundations of anonymity and secrecy protection should take probability into account.
In this cooperation, 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.
Our approach will be based on Information Theory. We believe that
the body of concepts and results related to the
notion of entropy, expressing the (lack of) information
in a random variable, will provide a natural and solid framework
for our goals.
1. Présentation du coordinateur étranger
Professor Panangaden received his Ph.D. in Physics from the University of Wisconsin in 1980, and a Master in Computer Science at the University of Utah, in 1985. After holding academic positions at Cornell University and at Queen's University, he joined the Department of Computer Science at McGill University. He has been invited speaker at a number of international conferences, including CONCUR'94, FSTTCS'95, PPDP'00, MFPS'01 and ISDT'04. He has been program committee chair of several conferences and workshops including EXPRESS'02, MFPS'03, and LICS'05. He is the Area Editor for Logic and Probability of the Journal on Logical Methods in Computer Science. He is also the author of 31 journal papers and 34 (refereed) conference papers, covering several research areas, including the theory of probabilistic systems, quantum computing, semantics for concurrent programming languages, and the relationships between logic and concurrent computation.
Présentation de l'équipe française
The French team is composed by Catuscia Palamidessi, some of the other members of the INRIA team Comète (see Point II.2. below for a more detailed description), and by Vincent Danos. Danos is not member of an INRIA team, but his current research interests are strongly related to this project, his background is in many ways complementary to that of Palamidessi, and he has an history of collaboration with Prakash Panangaden. Hence it seems very valuable for the project to involve him as a participant.
2. Historique de la collaboration
We have often regretted the lack of occasions to collaborate, since we believe our research wold have greatly benefited by combining our expertises and ways of reasoning. Usually we would discover only a posteriori that we had been working on similar problems, and be surprised by how much we had been driven by similar goals and how parallel our research paths had been.
Now we are both interested in a new subject, namely the development of a logic based on Information Theory, and its application to Security. We feel that, even more than in the past, the potential benefits of our collaboration are huge. Security is a central theme in the INRIA team Comète lead by Catuscia Palamidessi. She and other members of the group have contributed to the foundations of Anonymity, and have recently started studying Information Theory in view of its applications to Anonymity and Secrecy. Prakash Panangaden, besides his Master degree in Computer Science, has a PhD in Physics which makes him able to understand in depth the sophisticated concepts and techniques of Information Theory. Furthermore, Panangaden has a solid background in Logics and Category Theory, which have been main topics in his research for the last several years. In conclusion, in this project proposal we believe that we have an ideal situation, as we have the same interests, and competences which are in large part complementary.
The other members of Comète have not collaborated with Panangaden or other members of his team either.
On the other hand, Vincent Danos and Prakash Panangaden have already a long history of collaboration on topics related to the present proposal: Bisimulation for Probabilistic Systems, Approximations of Markov Processes, Conditional Expectation. The results of this collaboration have been published in prestigious conferences and journals (see first list of publications below). These works have contributed to deepen the understanding of probabilistic behaviors and models in computer systems, and they are therefore a reference point for some of the investigations we intend to pursue in this project.
Vincent Danos and Prakash Panangaden have also been collaborating on other topics not directly related to this proposal. In particular, they have been working together in Quantum Computing (see second list of publications below).
Joint publications related to the proposal
Joint publications not directly related to the proposal
To our knowledge there are the following ongoing collaborations between McGill and INRIA teams (the data are from the INRIA International - Cooperation with Canada web site)
3. Impact : indiquez en quoi, à votre avis, cette association aurait un impact important :
Not applicable in the case of Comète, since there are no previous collaborations.
We expect that also the INRIA project SECSI, leaded by Jean Goubault-Larrecq, will benefit from the visits of Prakash Panangaden and his team in Paris. The central theme of SECSI is Security, and the study of probabilistic aspects has an important role in that project.
SECSI and Comète are actually preparing a joint ARC proposal on the combination of nondeterminism and probability, with the goal of establishing the foundations for certain aspects of Security, and studying the possible implications for probabilistic Model Checking. Other partners in this proposal will be Vincent Danos, Marta Kwiatowska, and Roberto Segala. There are several possible relations between the two proposals, along the lines of Probability, Security, and Model Checking. If both proposal are accepted, we plan to organize a joint workshop in Paris, in summer 2006, in which all partners (from this project and the ARC one) are expected to participate.
In any case, the SECSI team will be kept informed about the visits of the McGill partners in Paris, and will be invited to attend to the talks and discussions that will take place during those occasions.
Two other groups at McGill that would be very much influenced by this work are the quantum information theory group headed by Claude Crepeau and Patrick Hayden and the machine learning group headed by Prof. Doina Precup and Joelle Pineau.
In the Quantum Information Theory group they study both quantum cryptography and foundational aspects of quantum information. There have already been extensive discussions between Panangaden, Patrick Hayden and John Yard (a visitor to Hayden's equipe) about Information Theory. There is an active collaboration between Panangaden, Pineau and Precup on aspects of probabilistic automata, duality and learning. The formulation of a logic of information would fit right in with aspects of learning probabilistic automata.
4. Divers : toute autre information que vous jugerez utile d'ajouter.
1. Foundations of Anonymity, Privacy, and Secrecy
Anonymity, privacy and secrecy are instances of a general issue that we could call partial hiding of information. Anonymity refers to keeping secret the identity of a user performing a certain action, while in general the effects of the action are supposed to become public. Privacy refers to the protection of certain data, like for instance the credit card number of a user, while making other data available. Secrecy, or Confidentiality, refers to the fact that certain information has to be kept hidden from certain users but not from others.
We intend to establish a theory of information-hiding based on the concept of entropy. Briefly, the idea is the following: Assuming that X is a random variable representing the information that we want to hide, and Y is the random variable representing the information that we want to make public, H(X|Y) (the entropy of X given Y) expresses the lack of information that we have w.r.t. X despite the complete knowledge of Y.
We plan to give a formal justification of the hierarchy of Reiter and Rubin  in our framework. This hierarchy is a classification of various degrees of anonymity protection that a protocol can achieve, and was defined only informally by Reiter and Rabin. For instance, we believe that Perfect Anonymity can be expressed in our framework by the formula H(X|Y) = H(X) (where H(X) is the entropy of X), i.e. the observation of Y does not reveal anything about X.
It is worth noting that, although there have been some attempts to define formally the above concepts, the definitions given in literature do not reflect what Reiter and Rubin have used in practice to prove the correctness of their protocols, see  for a discussion. An exception is represented by  and  which have formalized Strong Anonymity and Probable Innocence, although the definitions given there are rather ad hoc. We are confident that Information Theory will allow us to develop an elegant and unified theory for Anonymity and all the other information-hiding properties.
Participants: Prakash Panangaden, Kostas Chatzikokolakis, Catuscia Palamidessi
In many proofs in Information Theory there is a consistent repetitive
pattern. This can especially be noticed in channel capacity
theorems. We are seeking to abstract the logical (or categorical) essence
of these proofs and unify many of these ideas.
2. A Logic based on Information Theory
In searching a common logical core we are led to consider categories where Markov processes are captured naturally. There is a fundamental idea, due to Lawvere orginally but developed by Michele Giry, that one should work with the Kleisli category of the probabilistic powerset monad. This category, named SRel by Panangaden, has been studied as the category capturing the notion of stochastic relations . It turns out to have some interesting logical properties - it supports a nuclear ideal - and is an ideal candidate to start our study of the logic of probabilistic processes. The morphisms in this category are exactly Markov kernels and composition is just the composition of probabilistic transitions (what is called the Chapman-Kolmogorov equation in stochastic process theory) .
We plan to beging by asking how Information Theory fits in the SRel logic. Panangaden and his colleagues have already begun to look at this in the Quantum Information Theory setting.
Participants: Prakash Panangaden, Vincent Danos, Peng Wu
The formalism for describing the protocols should be suitable for verification,
that is, have a simple syntax and a clear semantics. Such formalism should allow to express concurrency,
communication, and quantitative aspects related to entropy. A process calculus, extended with
some kind of construct suitable
to represent random variables, seems therefore the natural choice. As a starting point,
the probabilistic pi-calculus of 
is a possible candidate. Suitable choices for the semantics include the
probabilistic bisimulations 
or the more ambitious approaches based on metrics ,
3. A process calculus and its semantics
In particular, in , Desharnais, Gupta, Jagadeesan and Panangaden have already started an information-theoretic investigation. They analyzed weak probabilistic bisimulation for a probabilistic process calculus with nondeterminism, probabilistic choice and hidden internal actions, and they developed a metric analogue of weak bisimulation. They showed that the channel capacity is a continuous function of the metric and they showed that all the process combinators are contractive in this metric.
One advantage of working with a process calculus is that it provides a natural framework to prove properties like compositionality of security. The channel capacity is a measure of the propensity of a system to leak information. If we have a system S in a context C[.], and we know that C[S] is secure, and if we know that S' is close to S according to the metric, then we know that C[S'] is secure as well since C[S'] must be close to C[S] (contractivity) and hence almost as secure (continuity of channel capacity). This is, of course, a preliminary intuition, but it shows that the recently developed quantitative tools (metric analogues of bismulation) for semantics of probabilistic process algebra will fit naturally with our idea of investigating security properties from an information-theoretic perspective.
Participants: Prakash Panangaden, Romain Beauxis, Catuscia Palamidessi, Peng Wu
In the long term, we expect our results to lay the foundations for automated verification techniques tailored to the information-hiding protocols. A good starting point could be the current probabilistic verification tools like PRISM. The extension we envisage would be based on the logic described in Point 2, on one hand, and the process-calculus formalism described in Point 3, on the other.
The verification of a property expressing protection of information will typically involve the calculation of some quantities related to entropy. We believe that this issue will lead to new perspectives in probabilistic model checking, and require totally new techniques.
In the long term, Panangaden and Palamidessi plan to have a PhD student in co-supervision who will investigate the above topics as his or her thesis project.
The French team is composed by:
The expected missions from the French team to McGill are the following: