Catálogo de publicaciones - libros

Sequence logic is a parameterized logic where the formulas are sequences of formulas of some arbitrary underlying logic. The sequence formulas are interpreted in certain linearly ordered sets of models of the underlying logic. This interpretation induces an entailment relation between sequence formulas which strongly depends on which orderings one wishes to consider. Some important classes are: all linear orderings, all dense linear orderings and all (or some specific) wellorderings.

For all these classes one can ask for a sound and complete proof system for the entailment relation, as well as for its decidability. For the class of dense linear orderings and all linear orderings we give sound and complete proof systems which also yield decidability (assuming that the underlying logic is sound, complete and decidable). We formulate some open problems on the entailment relation in the case of wellorderings.

This paper provides a new, decidable definition of the higher-order recursive path ordering in which type comparisons are made only when needed, therefore eliminating the need for the computability closure, and bound variables are handled explicitly, making it possible to handle recursors for arbitrary strictly positive inductive types.

We present Zenon, an automated theorem prover for first order classical logic (with equality), based on the tableau method. Zenon is intended to be the dedicated prover of the Focal environment, an object-oriented algebraic specification and proof system, which is able to produce OCaml code for execution and Coq code for certification. Zenon can directly generate Coq proofs (proof scripts or proof terms), which can be reinserted in the Coq specifications produced by Focal. Zenon can also be extended, which makes specific (and possibly local) automation possible in Focal.

In the area of Description Logic (DL) based knowledge representation, hybrid terminologies have been proposed as a means to make non-standard inference services available to knowledge bases that contain general concept inclusion (GCI) axioms. Building on existing work on subsumption in hybrid terminologies, the present paper provides the first in-depth investigation of the non-standard inferences least-common subsumer, and matching in hybrid -TBoxes; providing sound and complete algorithms for both inference services.

Many analysis techniques and decidability results have been obtained for cryptographic protocols. However all of them consider protocols with limited procedures for the processing of messages by agents or intruders: Information expected in a protocol message has to be located at a fixed position. However this is too restrictive for instance to model web-service protocols where messages are XML semi-structured documents and where significant information (name, signature, ...) has to be extracted from some nodes occurring at flexible positions. Therefore we extend the standard Dolev Yao intruder model by a subterm predicate that allows one to express a larger class of protocols that employs data extraction by subterm matching. This also allows one to detect so-called that are specific to web-services. In particular we show that protocol insecurity is decidable with complexity NP for finite sessions in this new model. The proof is not a consequence of the standard finite sessions case; on the contrary, it provides also a new short proof for this case.

In formal approaches, messages sent over a network are usually modeled by terms together with an equational theory, axiomatizing the properties of the cryptographic functions (encryption, exclusive or, ...). The analysis of cryptographic protocols requires a precise understanding of the attacker knowledge. Two standard notions are usually used: deducibility and indistinguishability. Only few results have been obtained (in an ad-hoc way) for equational theories with associative and commutative properties, especially in the case of static equivalence. The main contribution of this paper is to propose a general setting for solving deducibility and indistinguishability for an important class (called ) of these theories. Our setting relies on the correspondence between a monoidal theory E and a semiring  which allows us to give an algebraic characterization of the deducibility and indistinguishability problems. As a consequence we recover easily existing decidability results and obtain several new ones.

Transformation to continuation-passing style (CPS) is often performed by optimizing compilers for functional programming languages. As part of the development and proof of correctness of a compiler for the mini-ML functional language, we have mechanically verified the correctness of two CPS transformations for a call-by-value -calculus with -ary functions, recursive functions, data types and pattern-matching. The transformations generalize Plotkin’s original call-by-value transformation and Danvy and Nielsen’s optimized transformation, respectively. We used the Coq proof assistant to formalize the transformations and conduct and check the proofs. Originalities of this work include the use of big-step operational semantics to avoid difficulties with administrative redexes, and of two-sorted de Bruijn indices to avoid difficulties with -conversion.

Operational models of protocols, on one hand, are readable and conveniently match their implementation, at a certain abstraction level. Epistemic models, on the other hand, are appropriate for specifying knowledge-related properties such as anonymity. These two approaches to specification and analysis have so far developed in parallel and one has either to define ad hoc correctness criteria for the operational model or use complicated epistemic models to specify the operational behavior. We work towards bridging this gap by proposing a combined framework which allows modeling the behavior of a protocol in a process language with an operational semantics and supports reasoning about properties expressed in a rich logic with temporal and epistemic operators.

We propose a decision procedure, an inference system for clauses containing rigid and flexible variables. Rigid variables are only allowed to have one instantiation, whereas flexible variables are allowed as many instantiations as desired. We assume a set of clauses containing only rigid variables together with a set of clauses containing only flexible variables. When the flexible clauses fall into a particular class, we propose an inference system based on ordered resolution that is sound and complete and for which the inference procedure will halt.

An interest in this form of problem is for cryptographic protocol verification for a bounded number of protocol instances. Our class allows us to obtain a generic decidability result for a large class of cryptographic protocols that may use for instance CBC (Cipher Block Chaining) encryption and blind signature.

We extend the Description Logic with a “typicality” operator that allows us to reason about the prototypical properties and inheritance with exceptions. The resulting logic is called . The typicality operator is intended to select the “most normal” or “most typical” instances of a concept. In our framework, knowledge bases may then contain, in addition to ordinary ABoxes and TBoxes, subsumption relations of the form “() is subsumed by ”, expressing that typical -members have the property . The semantics of a typicality operator is defined by a set of postulates that are strongly related to Kraus-Lehmann-Magidor axioms of preferential logic . We first show that enjoys a simple semantics provided by ordinary structures equipped by a preference relation. This allows us to obtain a modal interpretation of the typicality operator. Using such a modal interpretation, we present a tableau calculus for deciding satisfiability of knowledge bases. Our calculus gives a nondeterministic-exponential time decision procedure for satisfiability of . We then extend knowledge bases by a nonmonotonic completion that allows inferring defeasible properties of specific concept instances.