Catálogo de publicaciones - libros

In this paper we extend the approximation based theoretical framework in which the security problem – secrecy preservation against an intruder – may be semi-decided through a reachability verification.

We explain how to cope with algebraic properties for an automatic approximation-based analysis of security protocols. We prove that if the initial knowledge of the intruder is a regular tree language, then the security problem may by semi-decided for protocols using cryptographic primitives with algebraic properties. More precisely, an automatically generated approximation function enables us 1) an automatic normalization of transitions, and 2) an automatic completion procedure. The main advantage of our approach is that the approximation function makes it possible to verify security protocols with an arbitrary number of sessions.

The concepts are illustrated on an example of the protocol using a cryptographic primitive with the exclusive or algebraic property.

The reachability problem as well as the computation of the phase portrait for the class of planar hybrid systems defined by constant differential inclusions (SPDI), has been shown to be decidable. The existing reachability algorithm is based on the exploitation of topological properties of the plane which are used to accelerate certain kind of cycles. The complexity of the algorithm makes the analysis of large systems generally unfeasible. In this paper we present a compositional parallel algorithm for reachability analysis of SPDIs. The parallelization is based on the qualitative information obtained from the phase portrait of an SPDI, in particular the controllability kernel.

Verification of multithreaded programs is difficult. It requires reasoning about state spaces that grow exponentially in the number of concurrent threads. Successful verification techniques based on modular composition of over-approximations of thread behaviors have been designed for this task. These techniques have been traditionally described in assume-guarantee style, which does not admit reasoning about the abstraction properties of the involved compositional argument. Flanagan and Qadeer thread-modular algorithm is a characteristic representative of such techniques. In this paper, we investigate the formalization of this algorithm in the framework of abstract interpretation. We identify the abstraction that the algorithm implements; its definition involves Cartesian products of sets. Our result provides a basis for the systematic study of similar abstractions for dealing with the state explosion problem. As a first step in this direction, our result provides a characterization of a minimal increase in the precision of the Flanagan and Qadeer algorithm that leads to the loss of its polynomial complexity.

Substitution is fundamental to computer science, underlying for example quantifiers in predicate logic and beta-reduction in the lambda-calculus. So is substitution something we define on syntax on a case-by-case basis, or can we turn the idea of ‘substitution’ into a mathematical object?

We exploit the new framework of Nominal Algebra to axiomatise substitution. We prove our axioms sound and complete with respect to a canonical model; this turns out to be quite hard, involving subtle use of results of rewriting and algebra.

Given a class of codes. A regular code in is called prime if it cannot be decomposed as a catenation of at least two non-trivial regular codes in . The prime decomposition problem for the class of codes consists in decomposing regular codes in into prime factors in . In this paper, a general approach to this problem is proposed, by means of which solutions for the prime decomposition problem are obtained, in a unified way, for several classes of codes. These classes are all subclasses of prefix codes and can be defined by binary relations.

We present a new approach to the determinisation process of specified types of automata using bit-parallel algorithms. We present the determinisation of nondeterministic pattern matching automata () for approximate pattern matching and we introduce the determinisation of suffix automata. This new approach speeds the determinisation up to times, where is the length of the pattern searched by , or accepted by the suffix automaton, respectively.

Alternating temporal logic (*) was introduced to prove properties of multi-agent systems in which the agents have different objectives and may collaborate to achieve them. Examples include (distributed) controlled systems, security protocols, and contract-signing protocols. Proving * properties over finite-state systems was shown decidable by Alur et al., and a model checker for the sublanguage implemented in .

In this paper we present a sound and complete proof system for proving * properties over infinite-state systems. The proof system reduces proofs of * properties over systems to first-order verification conditions in the underlying assertion language. The verification conditions make use of predicate transformers that depend on the system structure, so that proofs over systems with a simpler structure, e.g., turn-based systems, directly result in simpler verification conditions. We illustrate the use of the proof system on a small example.

Mainly concerned with type safety, Featherweight Java, or FJ, is a well known minimal core for Java and Generic Java. However, in the type system of FJ, the treatment of downcast is omitted. In this paper we propose a stronger type system for FJ and FGJ. In order to deal with the cast problems, we introduce some special techniques for types, and also strengthen the types for expressions and methods in terms of the type declaration notations. Supported by the type system and our techniques, we can ensure properties stronger than the ones proved in Igarashi ’s original FJ paper. Examples making the above mentioned contributions clear are illustrated throughout this paper. Furthermore a case study on design patterns showing the advantages of our results is given.

(PGs) were invented by John H. Conway and are described in his book . We formalize PGs in Higher Order Logic extended with ZF axioms (HOLZF) using Isabelle, a mechanical proof assistant. We show that PGs can be defined as the unique fixpoint of a function that arises naturally from Conway’s original definition. While the construction of PGs in HOLZF relies heavily on the ZF axioms, operations on PGs are defined on a game type that hides its set theoretic origins. A polymorphic type of sets that are not bigger than ZF sets facilitates this. We formalize the induction principle that Conway uses throughout his proofs about games, and prove its correctness. For these purposes we examine how the notions of well-foundedness in HOL and ZF are related in HOLZF. Finally, games (modulo equality) are added to Isabelle’s numeric types by showing that they are an instance of the axiomatic type class of partially ordered abelian groups.

Proof-producing program analysis augments the invariants inferred by an abstract interpreter with their correctness proofs. If these invariants are precise enough to guarantee safety, this method is an automatic verification tool. We present proof-synthesis algorithms for a simple flow chart language and domains mapping variables to abstract values and discuss some benefits for proof carrying code systems. Our work has been carried out in Isabelle/HOL and incorporated within a verified proof carrying code system.