arXiv subjects
Publications and source records attributed to David Baelde.
We generalize the validity criterion for the infinitary proof system of the multiplicative additive linear logic with fixed points. Our criterion is designed to take into account axioms and cuts. We show that it is sound and enjoys the cut elimination property. We finally study its decidability properties, and prove that it is undecidable in general but becomes decidable under some restrictions.
Formal methods have proved effective to automatically analyze protocols. Over the past years, much research has focused on verifying trace equivalence on protocols, which is notably used to model many interesting privacy properties, e.g., anonymity or unlinkability. Many tools for checking trace equivalence rely on a naive and expensive exploration of all interleavings of concurrent actions, which calls for partial-order reduction (POR) techniques. In this paper, we present the first POR technique for protocol equivalences that does not rely on an action-determinism assumption: we recast the trace equivalence problem as a reachability problem, to which persistent and sleep set techniques can be applied, and we show how to effectively apply these results in the context of symbolic executions. We report on a prototype implementation, improving the tool DeepSec.
In this paper, we consider the problem of verifying anonymity and unlinkability in the symbolic model, where protocols are represented as processes in a variant of the applied pi calculus, notably used in the ProVerif tool. Existing tools and techniques do not allow to verify directly these properties, expressed as behavioral equivalences. We propose a different approach: we design two conditions on protocols which are sufficient to ensure anonymity and unlinkability, and which can then be effectively checked automatically using ProVerif. Our two conditions correspond to two broad classes of attacks on unlinkability, i.e. data and control-flow leaks. This theoretical result is general enough that it applies to a wide class of protocols based on a variety of cryptographic primitives. In particular, using our tool, UKano, we provide the first formal security proofs of protocols such as BAC and PACE (e-passport), Hash-Lock (RFID authentication), etc. Our work has also lead to the discovery of new attacks, including one on the LAK protocol (RFID authentication) which was previously claimed to be unlinkable (in a weak sense).
Many privacy-type properties of security protocols can be modelled using trace equivalence properties in suitable process algebras. It has been shown that such properties can be decided for interesting classes of finite processes (i.e., without replication) by means of symbolic execution and constraint solving. However, this does not suffice to obtain practical tools. Current prototypes suffer from a classical combinatorial explosion problem caused by the exploration of many interleavings in the behaviour of processes. M\"odersheim et al. have tackled this problem for reachability properties using partial order reduction techniques. We revisit their work, generalize it and adapt it for equivalence checking. We obtain an optimisation in the form of a reduced symbolic semantics that eliminates redundant interleavings on the fly. The obtained partial order reduction technique has been integrated in a tool called APTE. We conducted complete benchmarks showing dramatic improvements.
Security protocols are concurrent processes that communicate using cryptography with the aim of achieving various security properties. Recent work on their formal verification has brought procedures and tools for deciding trace equivalence properties (e.g., anonymity, unlinkability, vote secrecy) for a bounded number of sessions. However, these procedures are based on a naive symbolic exploration of all traces of the considered processes which, unsurprisingly, greatly limits the scalability and practical impact of the verification tools. In this paper, we overcome this difficulty by developing partial order reduction techniques for the verification of security protocols. We provide reduced transition systems that optimally eliminate redundant traces, and which are adequate for model-checking trace equivalence properties of protocols by means of symbolic execution. We have implemented our reductions in the tool Apte, and demonstrated that it achieves the expected speedup on various protocols.
Many privacy-type properties of security protocols can be modelled using trace equivalence properties in suitable process algebras. It has been shown that such properties can be decided for interesting classes of finite processes (i.e., without replication) by means of symbolic execution and constraint solving. However, this does not suffice to obtain practical tools. Current prototypes suffer from a classical combinatorial explosion problem caused by the exploration of many interleavings in the behaviour of processes. M\"odersheim et al. have tackled this problem for reachability properties using partial order reduction techniques. We revisit their work, generalize it and adapt it for equivalence checking. We obtain an optimization in the form of a reduced symbolic semantics that eliminates redundant interleavings on the fly.
This volume contains the proceedings of the Ninth Workshop on Fixed Points in Computer Science which took place on the September 1st, 2013 in Torino, Italy as a CSL-affiliated workshop. Past workshops have been held in Brno (1998, MFCS/CSL workshop), Paris (2000, LC workshop), Florence (2001, PLI workshop), Copenhagen (2002, LICS (FLoC) workshop), Warsaw (2003, ETAPS workshop), Coimbra (2009, CSL workshop), Brno (2010, MFCS-CSL workshop), Tallinn (2012, CSL workshop). Fixed points play a fundamental role in several areas of computer science. They are used to justify (co)recursive definitions and associated reasoning techniques. The construction and properties of fixed points have been investigated in many different settings such as: design and implementation of programming languages, logics, verification, databases. The aim of this workshop is to provide a forum for researchers to present their results to those members of the computer science and logic communities who study or apply the theory of fixed points.
Inductive and coinductive specifications are widely used in formalizing computational systems. Such specifications have a natural rendition in logics that support fixed-point definitions. Another useful formalization device is that of recursive specifications. These specifications are not directly complemented by fixed-point reasoning techniques and, correspondingly, do not have to satisfy strong monotonicity restrictions. We show how to incorporate a rewriting capability into logics of fixed-point definitions towards additionally supporting recursive specifications. In particular, we describe a natural deduction calculus that adds a form of "closed-world" equality - a key ingredient to supporting fixed-point definitions - to deduction modulo, a framework for extending a logic with a rewriting layer operating on formulas. We show that our calculus enjoys strong normalizability when the rewrite system satisfies general properties and we demonstrate its usefulness in specifying and reasoning about syntax-based descriptions. The integration of closed-world equality into deduction modulo leads us to reconfigure the elimination principle for this form of equality in a way that, for the first time, resolves issues regarding the stability of finite proofs under reduction.
Generating multimedia streams, such as in a netradio, is a task which is complex and difficult to adapt to every users' needs. We introduce a novel approach in order to achieve it, based on a dedicated high-level functional programming language, called Liquidsoap, for generating, manipulating and broadcasting multimedia streams. Unlike traditional approaches, which are based on configuration files or static graphical interfaces, it also allows the user to build complex and highly customized systems. This language is based on a model for streams and contains operators and constructions, which make it adapted to the generation of streams. The interpreter of the language also ensures many properties concerning the good execution of the stream generation.
The first-order theory of MALL (multiplicative, additive linear logic) over only equalities is an interesting but weak logic since it cannot capture unbounded (infinite) behavior. Instead of accounting for unbounded behavior via the addition of the exponentials (! and ?), we add least and greatest fixed point operators. The resulting logic, which we call muMALL, satisfies two fundamental proof theoretic properties: we establish weak normalization for it, and we design a focused proof system that we prove complete. That second result provides a strong normal form for cut-free proof structures that can be used, for example, to help automate proof search. We show how these foundations can be applied to intuitionistic logic.
Dependently typed lambda calculi such as the Logical Framework (LF) are capable of representing relationships between terms through types. By exploiting the "formulas-as-types" notion, such calculi can also encode the correspondence between formulas and their proofs in typing judgments. As such, these calculi provide a natural yet powerful means for specifying varied formal systems. Such specifications can be transformed into a more direct form that uses predicate formulas over simply typed lambda-terms and that thereby provides the basis for their animation using conventional logic programming techniques. However, a naive use of this idea is fraught with inefficiencies arising from the fact that dependently typed expressions typically contain much redundant typing information. We investigate syntactic criteria for recognizing and, hence, eliminating such redundancies. In particular, we identify a property of bound variables in LF types called "rigidity" and formally show that checking that instantiations of such variables adhere to typing restrictions is unnecessary for the purpose of ensuring that the overall expression is well-formed. We show how to exploit this property in a translation based approach to executing specifications in the Twelf language. Recognizing redundancy is also relevant to devising compact representations of dependently typed expressions. We highlight this aspect of our work and discuss its connection with other approaches proposed in this context.
Dependently typed lambda calculi such as the Logical Framework (LF) can encode relationships between terms in types and can naturally capture correspondences between formulas and their proofs. Such calculi can also be given a logic programming interpretation: the Twelf system is based on such an interpretation of LF. We consider here whether a conventional logic programming language can provide the benefits of a Twelf-like system for encoding type and proof-and-formula dependencies. In particular, we present a simple mapping from LF specifications to a set of formulas in the higher-order hereditary Harrop (hohh) language, that relates derivations and proof-search between the two frameworks. We then show that this encoding can be improved by exploiting knowledge of the well-formedness of the original LF specifications to elide much redundant type-checking information. The resulting logic program has a structure that closely resembles the original specification, thereby allowing LF specifications to be viewed as hohh meta-programs. Using the Teyjus implementation of lambdaProlog, we show that our translation provides an efficient means for executing LF specifications, complementing the ability that the Twelf system provides for reasoning about them.
Bedwyr is a generalization of logic programming that allows model checking directly on syntactic expressions possibly containing bindings. This system, written in OCaml, is a direct implementation of two recent advances in the theory of proof search. The first is centered on the fact that both finite success and finite failure can be captured in the sequent calculus by incorporating inference rules for definitions that allow fixed points to be explored. As a result, proof search in such a sequent calculus can capture simple model checking problems as well as may and must behavior in operational semantics. The second is that higher-order abstract syntax is directly supported using term-level $λ$-binders and the $\nabla$ quantifier. These features allow reasoning directly on expressions containing bound variables.