Papers & Software





Comète-Parsifal Seminar (Abstracts 2004)


2012 2011 2010 2009 2008 2007 2006 2005 2004
Dec 15Alexis Saurin Separation in the Lambda-mu-calculus
Dec 7Maria Grazia Vigliotti Electoral Systems in Ambient Calculi
Nov 30Tom Chothia The Price of Guessing, in the pi-calculus
Nov 29Axelle Ziegler A format of congruence for open bisimulation in name-passing calculi
Nov 16Yuxin Deng Axiomatizations for probabilistic finite-state behaviors
Nov 9Andre Schiper Group Communication: where are we today and future challenges
Oct 26Bernadette Charron-Bost Reductions in Distributed Computing and applications to Agreement Tasks
Oct 19Kostas Chatzikokolakis Specification and Verification of Probabilistic Security Protocols
Oct 12Dale Miller Proof Search and Model Checking: An exploratory talk
Oct 6Jun Pang Verifying a Sliding Window Protocol in mCRL
Sep 17Tom Chothia Type-based Distributed Access Control


Wednesday Dec 15, 2005, 3pm.
Title: Separation in the Lambda-mu-calculus
Speaker: Alexis Saurin

Having recalled the basics concerning lambda-mu-calculus introduced by Michel Parigot in order to extend Curry-Howard isomorphism to classical natural deduction I will present a result by Rene' David and Walter Py showing that Separation property (often refered to as Bo"hm theorem) is not satisfied in lambda-mu-calculus.

We will then consider how to recover the property by analyzing what is the reason for its failure in the original calculus. The resulting calculus, the Lambda-mu-caluclus for which Separation property holds will be compared to Parigot's calculus and with a variant introduced by Philippe de Groote. We will in particular see how Lambda-mu can be considered as a calculus of terms and streams of terms.


Sept 17, 2004
Speaker: Tom Chothia
Title: "Type-based Distributed Access Control"


I will present a type system that combines a weak form of information flow control, termed distributed access control, with typed cryptographic operations. The motivation is to have a type system that ensures access control while giving the application the responsibility to secure network communications, and to do this safely. The notion of declassification certificates is introduced to support the declassification of encrypted data.

Purely local type checking is extended to distributed systems by associating access control lists with cryptographic keys. When a piece of data is sent outside of a type checked area it is encrypted with a key that represents the list of principles that can access that data. When encrypted data is received, the access restrictions from the decryption key are used as the access control type.

This work was carried out with Dominic Duggan and Jan Vitek.

October 6, 2004.
Speaker: Jun PANG
Title: "Verifying a Sliding Window Protocol in mCRL"

Within the process algebraic community, much effort has been spent on analyzing sliding window protocols. Aart Middeldorp (1986) and Jacob Brunekreef (1993) gave specifications in ACP and PSF, respectively. Frits Vaandrager (1986), Richard Groenveld (1987), Jos van Wamel (1992) and Marc Bezem and Jan Friso Groote (1994) manually verified one-bit sliding window protocols, in which the size of the sending and receiving window is one. Starting in 1990, we attempted to prove the most complex sliding window protocol (not taking into account additional features such as duplex message passing and piggybacking) from Tanenbaum's "Communication Protocols" correct using mCRL. This turned out to be unexpectedly hard, which is shown by the 13 year it took to complete this work.

We prove the correctness of a sliding window protocol with an arbitrary finite window size n and sequence numbers modulo 2n. We show that the sliding window protocol is branching bisimilar to a queue of capacity 2n. The proof is given entirely on the basis of an axiomatic theory, and was checked with the help of PVS.

(This is joint work with Bahareh Badban, Wan Fokkink , Jan Friso Groote and Jaco van de Pol.)

Oct 12, 2004
Title: Proof Search and Model Checking: An exploratory talk
Speaker: Dale Miller

Proof Search is a updating of the logic programming paradigm where proof theory is used to motivation new designs. A great deal of work in proof theory and computation has taken place in recent years. One recent development has been the development of a good proof theory for defined predicates, which is closely related to reasoning within fixpoints and to the closed-world-assumption.

In this talk, I will illustrate some recent results in this area, present many different examples, and demonstrate a recent prototype system, Level 0/1, by Alwen Tiu. I hope to explore to what extent this work on logic and its implementation might have in doing (symbolic) model checking.

Some related paper: Some of the following paper focus on higher-order abstract syntax and the nabla; quantifier. I will not focus on these aspects of this work in this talk: instead, the focus will be on first-order logic.

- Encoding Transition Systems in Sequent Calculus, by Raymond McDowell, Dale Miller, and Catuscia Palamidessi.

- Level 0/1 Prover, by Alwen Tiu.

- A Proof Theory for Generic Judgments, by Dale Miller and Alwen Tiu.

- A Proof Search Specification of the pi-Calculus, by Alwen Tiu and Dale Miller.

Oct 19, 2004.
Title: Specification and Verification of Probabilistic Security Protocols
Speaker: Kostas Chatzikokolakis

Security protocols provide the ability of communicating privately using public means. A certain category of such protocols rely on probabilistic decisions and use primitives such as the Oblivious Transfer. Even though probabilistic protocols have been studied using model checking methods, little attempt of applying process calculi techniques has been made.

In this talk, we use a probabilistic variant of pi-calculus in order to model probabilistic protocols. We present a method of expressing some desired properties of such protocols which involves the construction of a proper specification and the introduction of a suitable precongruence relation between processes. We finally apply our method to the Partial Secrets Exchange protocol and prove its fairness.

Oct 26, 2004.
Title: Reductions in Distributed Computingn and applications to Agreement Tasks.
Speaker: Bernadette Charron-Bost

In this talk, we introduce several notions of reduction in distributed computing, and investigate reduction properties of two fundamental agreement tasks, namely Consensus and Atomic Commitment.

We first propose the notion of reduction "à la Karp", an analog for distributed computing of the classical Karp reduction. We then define a weaker reduction which is the analog of Cook reduction. These two reductions are called K- reduction and C-reduction, respectively.

We establish various reducibility and irreducibility theorems with respect to these two reductions. Our main result is an incomparability statement for Consensus and Atomic Commitment tasks: we show that they are incomparable with respect to the C-reduction, except when the resiliency degree is 1, in which case Atomic Commitment is strictly harder than Consensus. A side consequence of these results is that our notion of C-reduction is strictly weaker than the one of K-reduction.

Finally, we introduce a third notion of reduction which measures the hardness to solve a task in terms of the information about failures required to solve the task. We prove that this latter reduction is strictly weaker than the C-reduction. In other words, the information about failures -- or equivalently, the weakest failure detector -- needed to solve a task does not entirely capture the hardness of the task.


Nov 9, 2004
Title: Group Communication: where are we today and future challenges.
Speaker: André Schiper

Group communication is a topic studied since more than twenty years. During this period significant results have been obtained. Nevertheless there are issues that have not been addressed adequately. The paper presents both the important results related to group communication that have been obtained, but also points out what remains to be done to make group communication widely used, and as successful as some of the existing middleware technologies.

Nov 16, 2004
Title: Axiomatizations for probabilistic finite-state behaviors
Speaker: Yuxin Deng

We study a process calculus which combines both nondeterministic and probabilistic behavior in the style of Segala and Lynch's probabilistic automata. We consider various strong and weak behavioral equivalences, and we provide complete axiomatizations for finite state processes, restricted to guarded definitions in case of the weak equivalences. We conjecture that in the general case of unguarded recursion the ``natural'' weak equivalences are undecidable. This is the first work, to our knowledge, that provides a complete axiomatization for weak equivalences in the presence of recursion and both nondeterministic and probabilistic choice.


Mon Nov 29, 2004
Title: A format of congruence for open bisimulation in name-passing calculi
Speaker: Axelle Ziegler

In this talk, I'll present the use a general formal framework encoding name-passing process calculi and allowing to reason about them, using the nabla quantifier, definitions and higher-order abstract syntax. I'll show how this framework can be used to specify a format for bisimulation to be a congruence. Finally, I'll try to sketch what a model of this theory could be, and how it would connect with our applied result.

Tue Nov 30, 2004, 3pm.
Title: The Price of Guessing, in the pi-calculus. (with an Introduction to Formal and Computational Protocol Checking )
Speaker: Tom Chothia

I will present an outline of formal and computational methods that can be used to "prove" a process secure and I will outline some the problems with these methods; this will be a basic introduction aimed at formal methods people who do not have a back ground in security. I will then describe some of the work that has been done to bridge the gap between these formal and computational worlds, which mostly consists of finding computational criteria that, when met, ensure that formal analysis and computation coincide. Finally, I will suggest a new line of work that I am undertaking, which involves extending the pi-calculus with primitives for guessing new names and a method of finding the cost of a trace that will allow analysis that approximates computational methods without the need to do any difficult computational proofs. This new work is in a very early stage and so will be largely conjecture.

Mon May 2 2004. 3pm
Speaker: Brigitte Pientka
Title:Overcoming Performance Barriers: efficient proof search in logical frameworks


The logical framework Twelf provides an experimental platform to specify, implement and execute formal systems. One of its applications is in proof-carrying code and proof-carrying authentication, where it is successfully used to specify and verify formal guarantees about the run-time behavior of programs. These real-world applications have exposed some critical bottlenecks: execution of many logical specifications is severely hampered and some are not executable at all, thereby limiting its application in practice.

In this talk, I will describe three optimizations which substantially improve the performance and extend the power of the existing system. First, I give an optimized unification algorithm for logical frameworks which allows us to eliminate unnecessary occurs-checks. Second I present a novel execution model based on selective memoization and third I will discuss term indexing techniques to sustain performance in large-scale examples. As experimental results will demonstrate, these optimizations taken together constitute a significant step toward exploring the full potential of logical frameworks in real-world applications.


Dec 7, 2005, 3pm.
Title: Electoral Systems in Ambient Calculi
Speaker: Maria Grazia Vigliotti, Imperial College, London

This work compares the expressiveness of ambient calculi against different dialects of the pi-calculus. Cardelli and Gordon encoded the asynchronous pi-calculus into the ambient calculus (Mobile Ambients). Zimmer has shown that the synchronous pi-calculus without choice can be encoded in pure (no communication) Safe Ambients. We show that the pure ambient calculus without restriction has symmetric electoral systems, that is, it is possible to solve the problem of electing a leader in a symmetric network. By the work of Palamidessi, this implies that this fragment of the ambient calculus is not encodable (under certain conditions) in the pi-calculus with separate choice.

Not scheduled yet
Title: On Infinite Satisfaction and Behaviour
Speaker: Frank D. Valencia

Finite state models prevail in today's specification and verification techniques. Global Computing systems are, however, inherently open --e.g., typically there is no bound on the number of resources/devices that can be added to a given system. So, the assumption I shall be working with is that many phenomena in Global Computing are best described in infinite-state models.

In this talk I shall give an overview of my current interests and work on infinite behavior in two areas of computer science: Concurrency Theory and Computability. Concerning the former, I shall give an overview of my work on the expressive power of different ways of specifying infinite-behaviour in process calculi. As for the latter, I shall introduce a new framework for Infinite Satisfaction Problems (basically, Infinite SAT Problems) and present some (un)decidability results we have identified for this kind of problems. These results have an impact on Open Constraint Problems; a framework recently introduced for constraint problems in Global Computing scenarios.

My work on infinite satisfaction and behaviour involves several co-authors. The following list of relevant work acknowledges all of them:

- Stefan Dantchev and Frank D. Valencia. On the Computational Limits of Infinite Satisfaction. In SAC2005. © ACM Press, March 2005.

- C. Palamidessi, V. Saraswat, B. Victor, F. Valencia. Linearity vs Persistency in the Pi Calculus. Ongoing work.

- Pablo Giambiagi, Gerardo Schneider, Frank D. Valencia. On the Expressiveness of Infinite Behavior and Name Scoping in Process Calculi. In Proceedings of FOSSACS 04. LNCS, ©Springer-Verlag. March. 2004.

- Frank D. Valencia. Decidability of Infinite-State Timed CCP Process and First-Oder LTL. To appear in Theoretical Computer Science. © Elsevier.

- Mogens Nielsen, Catuscia Palamidessi and Frank D. Valencia. On the Expressive Power of Temporal Concurrent Constraint Programming Languages. In PPDP 2002. © ACM Press Oct. 2002

Page maintainer: Carlos Olarte