Propositions de stage de DEA
Stages available on the following subjects:
Catuscia
Palamidessi, INRIA-Futurs and LIX.
Description du sujet
After the seminal work of Abadi and Gordon on the spi calculus,
there have been several proposals of process
calculi-based frameworks for the specification and verification of
security protocols. The idea in general is to model the parties
involved (the righteous parties, the server, the adversary) as
communicating processes, and then specify/verify the protocols in terms of
properties of the intended behavior of the system.
We have two stage proposals on this topic:
-
One characteristics of most of the approaches described above
is that they deal with security protocols at a certain level of
abstraction, namely within the Dolev-Yao model of adversary which is
based on the assumption of ``perfect encryption''. If one wants to
analyze the correctness of security protocols at a finer level,
however, then it becomes necessary to use a probabilistic framework.
The task of the stage will be the development of a probabilistic calculus,
possibly based on the pi-calculus, suitable for the formal treatment
of security protocols. We envisage possible applications also in the
area of probabilistic security protocols.
-
In order to make the analysis feasible, the system behavior needs to be
described at a symbolic level. One of the main techniques is to use
symbolic unification or constraints in the treatment of
communication.
The combination of process calculi and unification/constraints,
however, until now has been done in a rather ad-hoc way.
We propose to develop, instead, a new calculus based on
the well studied and elegant paradigms of
Concurrent Constraint Programming and on the pi-calculus.
The purpose of the stage will be the design of this langauge,
the investigation of its properties, and the application to some case
study in security protocols.
It will be possible to continue this work as a PhD student.
Bibliography
- (Both stages)
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].
- (Stage 1) P. Mateus, J.C. Mitchell, and A. Scedrov.
Composition of cryptographic protocols
in a probabilistic polynomial-time process calculus.
In: R. Amadio and D. Lugiez, eds.,
"CONCUR 2003 - Concurrency Theory",
14-th International Conference, Marseille, France, September 2003,
Springer LNCS Volume 2761, Springer-Verlag, 2003, pp. 327-349.
[
ps]
- (Stage 1) G. Norman and V. Shmatikov. Analysis of probabilistic contract signing.
In BCSFACS Formal Aspects of Security (FASec '02), 2002.
[ps]
- (Stage 1) Mihaela Herescu and Catuscia Palamidessi.
Probabilistic asynchronous $\pi$-calculus.
In Jerzy Tiuryn, editor, Proceedings of FOSSACS 2000
(Part of ETAPS 2000), volume 1784 of
Lecture Notes in Computer Science, pages 146--160. Springer-Verlag, 2000.
[ps of report version.]
- (Stage 2) Michele Boreale, Marzia Buscemi. A Framework for the Analysis of
Security Protocol. In Proc. of CONCUR '02, LNCS 2421,
Springer-Verlag, 2002.
[ps]
- (Stage 2) Marcelo Fiore and Martín Abadi. Computing symbolic models for verifying
cryptographic protocols.
In Proc. 14th IEEE Computer Security Foundations Workshop, pages 160--173, 2001.
[ps]
- (Stage 2) Frank S. de Boer, Alessandra Di Pierro, and Catuscia Palamidessi.
Infinite computations in nondeterministic constraint programming.
Theoretical Computer Science,
151(1):37-78, 1995.
[ps]
Catuscia
Palamidessi, INRIA-Futurs and LIX.
Description du sujet
|
Beware of the Turing tar-pit in which everything
is possible but nothing of interest is easy.
|
|
Alan Perlis, 1982
|
Alan Perlis' famous epigram means that in Programming Languages one should not reduce
expressiveness to Turing-completeness. This is even more true nowadays,
since the advent of new computational paradigms like concurrency and
mobility have added new and rich dimensions in which the notion of
expressive power can be explored. The main challenges include
questions like "In which sense concurrent computation is more
expressive than sequential computation"? and "In which sense is
language X more suitable for distributed programming than language Y?"
Although these goals are ambitious, many think that this is one of the
most exciting research directions in Theoretical
Computer Science nowadays, and there is even an annual symposium
(EXPRESS) dedicated to it.
This is, to my opinion, a very stimulating area of research, and there
are several open questions
that can be the subject of a stage project, at various level of
difficulty. I list here two of them to give an idea:
- Process calculi are usually based on point-to-point
communication because it is considered more basic than other forms of
communication. Recent research, however, indicates that for certain
applications a different model is more effective and may even be more
primitive. This is the case, for instance, of broadcasting. The
project consists in checking this conjecture by
comparing the expressive power of point-to-point
communication vs broadcasting in CCS and in the pi-calculus.
- Recent works have pointed out an apparent
inconsistency: repCCS (which is CCS with replication instead of
recursion) is Turing-complete, in the sense that it can
nondeterministically emulate a Turing machine. However, termination
in repCCS is decidable (sic!). This findings suggest that
nondeterminism in concurrency is somehow richer than in sequential
computation. The project consists in formalizing and exploring the
implications of this observation.
It will be possible to continue this work as a PhD student.
Bibliography
-
Luca Aceto, Giuseppe Longo and Björn Victor editors.
Mathematical Structures in Computer Science, 13(4) (2003),
Special issue devoted to "The Difference between Concurrent and
Sequential Computation". [Foreword]
-
Catuscia Palamidessi. Comparing the Expressive Power of the Synchronous and the Asynchronous
pi-calculus.
Mathematical Structures in Computer Science, 13(4) (2003).
pp. 685-719.
[pdf,
postscript.]
- Uwe Nestmann and Benjamin C. Pierce.
Decoding Choice Encodings.
Journal of Information & Computation. 163(1): 1-59 (Nov 2000).
Latest version available as BRICS Report RS-99-42.
-
Nadia Busi, Maurizio Gabbrielli, Gianluigi Zavattaro. Replication vs. Recursive Definitions
in Channel Based Calculi. In Proc. of Thirtieth International Colloquium
on Automata, Languages and Programming (ICALP'03), 133-144 LNCS 2719, Springer-Verlag,
2003. [Postscript]
Dale
Miller, INRIA-Futurs and LIX, Ecole Polytechnique, and
Catuscia
Palamidessi, INRIA-Futurs and LIX.
Description du sujet
There are a number of restrictions on the specification of operational
semantics of process calculi that guarantee that the resulting
bisimulation relation is a congruence. These restrictions are known
variously as de Simone format, GSOS, tyft/tyxt, etc. To date, all
this work has been carried our for systems described via first-order
terms and first-order logic inference rules.
While a number of higher-order process calculi and calculi for
mobility of names and links have been studied, no general syntactic
restrictions are know for such calculi that parallel the results for
first-order systems. This stage will attempt to develop such
restrictions. The use of higher-order meta-logic and higher-order
abstract syntax is hoped to provide a strong basis for this work.
It will be possible to continue this work as a PhD student.
Bibliography
The following bibliography is indicative of the kind of papers that
will be part of this research effort.
Robert de
Simone. Higher-level synchronising devices in meije--SCCS.
Theoretical Computer Science, 37:245--267, 1985.
Jan Friso Groote and Frits Vaandrager.
Structured operational semantics and bisimulation as a congruence. Information and
Computation, vol 100, pp. 202-260 (1992).
Bard Bloom, Sorin Istrail,
and Albert R. Meyer.
Bisimulation Can't be Traced. Journal of the ACM, 42(1), January 1995,
pp. 232-268.
[pdf].
Douglas J. Howe.
Proving Congruence of Bisimulation in Functional Programming
Languages.
Information and Computation 124(2), pp. 103--112 (1996).
Karen L. Bernstein.
A Congruence Theorem for Structured Operational Semantics of
Higher-Order Languages. In the Proceedings
of LICS '98, edited by John Mitchell, pp. 153-163.
[ps].
- Dale Miller and Catuscia Palamidessi.
Foundational Aspects of Syntax.
ACM Computing Surveys 31(3es):11, 1999.
[ps.]
Dale Miller and Alwen Tiu.
A Proof Theory for Generic Judgments.
Submitted to a special issue of the ACM Transactions on Computational
Logic, edited by Phokion Kolaitis.
[pdf].
Catuscia
Palamidessi