Rigid tree automata and applications

We introduce the class of rigid tree automata (RTA), an extension of standard bottom-up automata on ranked trees with distinguished states called rigid. Rigid states define a restriction on the computation of RTA on trees: RTA can test for equality in subtrees reaching the same rigid state. RTA are able to perform local and global tests of equality between subtrees, non-linear tree pattern matching, and some inequality and disequality tests as well. Properties like determinism, pumping lemma, Boolean closure, and several decision problems are studied in detail. In particular, the emptiness problem is shown decidable in linear time for RTA whereas membership of a given tree to the language of a given RTA is NP-complete. Our main result is the decidability of whether a given tree belongs to the rewrite closure of an RTA language under a restricted family of term rewriting systems, whereas this closure is not an RTA language. This result, one of the first on rewrite closure of languages of tree automata with constraints, is enabling the extension of model checking procedures based on finite tree automata techniques, in particular for the verification of communicating processes with several local non-rewritable memories, like security protocols. Finally, a comparison of RTA with several classes of tree automata with local and global equality tests, with dag automata and Horn clause formalisms is also provided.     

On the decidability of cryptographic protocols with open-ended data structures

Formal analysis of cryptographic protocols has concentrated mainly on protocols with closed-ended data structures, i.e., protocols where the messages exchanged between principals have fixed and finite format. In many protocols, however, the data structures used are open-ended, i.e., messages have an unbounded number of data fields. In this paper, decidability issues for such protocols are studied. We propose a protocol model in which principals are described by transducers, i.e., finite automata with output, and show that in this model security is decidable and PSPACE-hard in presence of the standard Dolev-Yao intruder.     

Relating symbolic and cryptographic secrecy

We investigate the relation between symbolic and cryptographic secrecy properties for cryptographic protocols. Symbolic secrecy of payload messages or exchanged keys is arguably the most important notion of secrecy shown with automated proof tools. It means that an adversary restricted to symbolic operations on terms can never get the entire considered object into its knowledge set. Cryptographic secrecy essentially means computational indistinguishability between the real object and a random one, given the view of a much more general adversary. In spite of recent advances in linking symbolic and computational models of cryptography, no relation for secrecy under active attacks is known yet. For exchanged keys, we show that a certain strict symbolic secrecy definition over a specific Dolev-Yao-style cryptographic library implies cryptographic key secrecy for a real implementation of this cryptographic library. For payload messages, we present the first general cryptographic secrecy definition for a reactive scenario. The main challenge is to separate secrecy violations by the protocol under consideration from secrecy violations by the protocol users in a general way. For this definition, we show a general secrecy preservation theorem under reactive simulatability, the cryptographic notion of secure implementation. This theorem is of independent cryptographic interest. We then show that symbolic secrecy implies cryptographic payload secrecy for the same cryptographic library as used in key secrecy. Our results thus enable formal proof techniques to establish cryptographically sound proofs of secrecy for payload messages and exchanged keys.     

Security properties: two agents are sufficient

We consider an important family of cryptographic protocols and a class of security properties which encompasses secrecy and authentication. We show that it is always sufficient to consider a bounded number of agents b (b = 2 for secrecy properties for example): if there is an attack involving n agents, then there is an attack involving at most b agents.     

Automata for Reduction Properties Solving

We introduce a new class of tree automata, which we call Reduction Automata (RA), and we use it to prove the decidability of the whole first order of theory of reduction (the theory of reduction is the set of true sentences built up with unary predicates red_t(x) "x is reducible by t", i.e. "some instance of t is a subterm of x"). So we link rewriting, logic and formal languages.     

Spinal-Formed Context-Free Tree Grammars

In this paper we introduce a restricted model of context-free tree grammars called spine grammars, and study their formal properties including considerably simple normal forms. Recent research on natural languages has suggested that formalisms for natural languages need to generate a slightly larger class of languages than context-free grammars, and for that reason tree adjoining grammars have been widely studied relating them to natural languages. It is shown that the class of string languages generated by spine grammars coincides with that of tree adjoining grammars. We also introduce acceptors called linear pushdown tree automata, and show that linear pushdown tree automata accept exactly the class of tree languages generated by spine grammars. Linear pushdown tree automata are obtained from pushdown tree automata with a restriction on duplicability for the pushdown stacks. Received May 29, 1998, and in revised form April 27, 1999, and in final form May 10, 1999.     

基于Petri网的密码协议分析

在Federico提出的一种密码协议进程语言的基础上，建立了便于进行密码协议分析的简化Petri网模型，给出了协议满足秘密性的充要条件，并以NS公钥协议为例，用Petri网模型，结合归纳方法和串空间分析方法从密钥、新鲜数和协议主体三个方面的秘密性分析了该协议的秘密性，简化了协议秘密性的分析。     

Weighted Picture Automata and Weighted Logics

We investigate formal power series on pictures. These are functions that map pictures to elements of a semiring and provide an extension of two-dimensional languages to a quantitative setting. We establish a notion of a weighted MSO logics over pictures. The semantics of a weighted formula will be a picture series. We introduce weighted 2-dimensional on-line tessellation automata (W2OTA) and prove that for commutative semirings, the class of picture series defined by sentences of the weighted logics coincides with the family of picture series that are computable by W2OTA. Moreover, we show that the family of behaviors of W2OTA coincide precisely with the class of picture series characterized by weighted (quadrapolic) picture automata and consequently, the notion of weighted recognizability presented here is robust. However, the weighted structures can not be used to get better decidability properties than in the language case. For every commutative semiring, it is undecidable whether a given MSO formula has restricted structure or whether the semantics of a formula has empty support.     

The reactive simulatability (RSIM) framework for asynchronous systems

We define reactive simulatability for general asynchronous systems. Roughly, simulatability means that a real system implements an ideal system (specification) in a way that preserves security in a general cryptographic sense. Reactive means that the system can interact with its users multiple times, e.g., in many concurrent protocol runs or a multi-round game. In terms of distributed systems, reactive simulatability is a type of refinement that preserves particularly strong properties, in particular confidentiality. A core feature of reactive simulatability is composability, i.e., the real system can be plugged in instead of the ideal system within arbitrary larger systems; this is shown in follow-up papers, and so is the preservation of many classes of individual security properties from the ideal to the real systems.A large part of this paper defines a suitable system model. It is based on probabilistic IO automata (PIOA) with two main new features: One is generic distributed scheduling. Important special cases are realistic adversarial scheduling, procedure-call-type scheduling among colocated system parts, and special schedulers such as for fairness, also in combinations. The other is the definition of the reactive runtime via a realization by Turing machines such that notions like polynomial-time are composable. The simple complexity of the transition functions of the automata is not composable.As specializations of this model we define security-specific concepts, in particular a separation between honest users and adversaries and several trust models.The benefit of IO automata as the main model, instead of only interactive Turing machines as usual in cryptographic multi-party computation, is that many cryptographic systems can be specified with an ideal system consisting of only one simple, deterministic IO automaton without any cryptographic objects, as many follow-up papers show. This enables the use of classic formal methods and automatic proof tools for proving larger distributed protocols and systems that use these cryptographic systems.     

Non-Linear Rewrite Closure and Weak Normalization

A rewrite closure is an extension of a term rewrite system with new rules, usually deduced by transitivity. Rewrite closures have the nice property that all rewrite derivations can be transformed into derivations of a simple form. This property has been useful for proving decidability results in term rewriting. Unfortunately, when the term rewrite system is not linear, the construction of a rewrite closure is quite challenging. In this paper, we construct a rewrite closure for term rewrite systems that satisfy two properties: the right-hand side term in each rewrite rule contains no repeated variable (right-linear) and contains no variable occurring at depth greater than one (right-shallow). The left-hand side term is unrestricted, and in particular, it may be non-linear. As a consequence of the rewrite closure construction, we are able to prove decidability of the weak normalization problem for right-linear right-shallow term rewrite systems. Proving this result also requires tree automata theory. We use the fact that right-shallow right-linear term rewrite systems are regularity preserving. Moreover, their set of normal forms can be represented with a tree automaton with disequality constraints, and emptiness of this kind of automata, as well as its generalization to reduction automata, is decidable. A preliminary version of this work was presented at LICS 2009 (Creus 2009).     

一种多项式时间复杂度的密码协议秘密性验证方法

密码协议的秘密性验证是网络安全领域的一个难题,本文在提出协议行为结构的基础上,通过对协议行为及其结构的分析,提出了一种新的密码协议的秘密性验证算法,该算法的时间复杂度是多项式时间的,从而简化了秘密性验证过程,文中最后,作为实例,给出了TMN密码协议的秘密性验证。     

Optimal reachability for multi-priced timed automata

In this paper, we prove the decidability of the minimal and maximal reachability problems for multi-priced timed automata, an extension of timed automata with multiple cost variables evolving according to given rates for each location. More precisely, we consider the problems of synthesizing the minimal and maximal costs of reaching a given target location. These problems generalize conditional optimal reachability, i.e., the problem of minimizing one primary cost under individual upper bound constraints on the remaining, secondary, costs, and the problem of maximizing the primary cost under individual lower bound constraints on the secondary costs. Furthermore, under the liveness constraint that all traces eventually reach the goal location, we can synthesize all costs combinations that can reach the goal.

The decidability of the minimal reachability problem is proven by constructing a zone-based algorithm that always terminates while synthesizing the optimal cost tuples. For the corresponding maximization problem, we construct two zone-based algorithms, one with and one without the above liveness constraint. All algorithms are presented in the setting of two cost variables and then lifted to an arbitrary number of cost variables.     

Alternating two-way AC-tree automata

We explore the notion of alternating two-way tree automata modulo the theory of finitely many associative-commutative (AC) symbols. This was prompted by questions arising in cryptographic protocol verification, in particular in modeling group key agreement schemes based on Diffie-Hellman-like functions, where the emptiness question for intersections of such automata is fundamental. This also has independent interest. We show that the use of general push clauses, or of alternation, leads to undecidability, already in the case of one AC symbol, with only functions of arity zero. On the other hand, emptiness is decidable in the general case of several function symbols, including several AC symbols, provided push clauses are unconditional and intersection clauses are final. This class of automata is also shown to be closed under intersection.     

Limits of the BRSIM/UC soundness of Dolev–Yao-style XOR

The abstraction of cryptographic operations by term algebras, called Dolev–Yao models, is essential in almost all tool-supported methods for proving security protocols. Recently significant progress was made in proving that Dolev–Yao models can be sound with respect to actual cryptographic realizations and security definitions. The strongest results show this in the sense of blackbox reactive simulatability (BRSIM)/UC, a notion that essentially means the preservation of arbitrary security properties under arbitrary active attacks and in arbitrary protocol environments, with only small changes to the Dolev–Yao models and natural implementations. However, these results are so far restricted to core cryptographic systems like encryption and signatures. Typical modern tools and complexity results around Dolev–Yao models also allow operations with more algebraic properties, in particular XOR because of its clear structure and cryptographic usefulness. We show that it is not possible to extend the strong BRSIM/UC results to XOR, at least not with remotely the same generality and naturalness as for the core cryptographic systems. We also show that for every potential soundness result for XOR with secrecy implications, one significant change to typical Dolev–Yao models must be made. On the positive side, we show the soundness of a rather general Dolev–Yao model with XOR and its realization in the sense of BRSIM/UC under passive attacks. A preliminary version of this paper appeared in Proc. 10th European Symposium on Research in Computer Security [9]     

Quantitative analysis of weighted transition systems

We present a general framework for the analysis of quantitative and qualitative properties of reactive systems, based on a notion of weighted transition systems. We introduce and analyze three different types of distances on weighted transition systems, both in a linear and a branching version. Our quantitative notions appear to be reasonable extensions of the standard qualitative concepts, and the three different types introduced are shown to measure inequivalent properties.When applied to the formalism of weighted timed automata, we show that some standard decidability and undecidability results for timed automata extend to our quantitative setting.     

Security by typing

We present an approach for analyzing cryptographic protocols that are subject to attack from an active intruder who takes advantage of knowledge of the protocol rules. The approach uses a form of type system in which types are communication steps and typing constraints characterize all the messages available to the intruder. This reduces verification of authentication and secrecy properties to a typing problem in our type system. We present the typing rules, prove soundness of a type inference algorithm, and establish the correctness of the typing rules with respect to the protocol execution and intruder actions. The protocol specifications used in the approach can be automatically extracted from the conventional, informal cryptographic protocol notation commonly found in the literature. To validate the approach, we implement our algorithm in a tool called DYMNA, which is a practical and efficient environment for the specification and analysis of cryptographic protocols.     

Algebra model and security analysis for cryptographic protocols

With the rapid growth of the Internet and the World Wide Web a large number of cryptographic protocols have been deployed in distributed systems for various application requirements, and security problems of distributed systems have become very important issues. There are some natural problems: does the protocol have the right properties as dictated by the requirements of the system? Is it still secure that multiple secure cryptographic protocols are concurrently executed? How shall we analy…     

Distributed synthesis for well-connected architectures

We study the synthesis problem for external linear or branching specifications and distributed, synchronous architectures with arbitrary delays on processes. External means that the specification only relates input and output variables. We introduce the subclass of uniformly well-connected (UWC) architectures for which there exists a routing allowing each output process to get the values of all inputs it is connected to, as soon as possible. We prove that the distributed synthesis problem is decidable on UWC architectures if and only if the output variables are totally ordered by their knowledge of input variables. We also show that if we extend this class by letting the routing depend on the output process, then the previous decidability result fails. Finally, we provide a natural restriction on specifications under which the whole class of UWC architectures is decidable.     

Pushdown tree automata

We define topdown pushdown tree automata (PDTA's) which extend the usual string pushdown automata by allowing trees instead of strings in both the input and the stack. We prove that PDTA's recognize the class of context-free tree languages. (Quasi)realtime and deterministic PDTA's accept the classes of Greibach and deterministic tree languages, respectively. Finally, PDTA's are shown to be equivalent to restricted PDTA's, whose stack is linear: this both yields a more operational way of recognizing context-free tree languages and connects them with the class of indexed languages.     

Preface: Volume 55, Issue 1

This volume contains the Proceedings of the First Workshop on Logical Aspects of Cryptographic Protocol Verification (LACPV'2001), held in Paris, France, July 23, 2001 as a satellite workshop of CAV'01.Security of computer systems is a growing field of concerns. While security in the large is quite a large and daunting field, the study of cryptographic protocols has received renewed interest in recent years, mostly because of the emergence of electronic commerce. The focus in cryptographic protocols, as opposed to mere cryptography, is the interaction of cryptographic primitives with message exchanges and possible malevolent actions from intruders. Most of the discovered bugs in cryptographic protocols are not so much tied to subtleties in cryptography, rather to logical aspects of interactions between principals.From a protocol-oriented point of view, cryptographic protocols pose new challenges: there may be an unbounded number of principals (processes in parallel), state spaces are infinite even with bounded numbers of principals, and so on. Several models exist that handle the complexity of cryptographic protocol verification, based on process calculi, first-order logic, automata theory, complexity theory among others.As such, cryptographic protocol verification is emerging as a research field in its own right, strongly linked to logic. The purpose of the LACPV workshop is to bring together researchers in the field of cryptographic protocol verification to share new results in the field. Domains of interest include formal relationships between models of cryptographic protocols, translations, expressive power; comparison between verification methods, accuracy, efficiency; fragments of first-order logic or extensions corresponding to various problems of interest in cryptographic protocol verification; decidability and complexity of cryptographic verification problems, reachability, decidable subcases; new logics and calculi for verifying cryptographic protocols; new approaches to reduce state spaces from infinite to finite; logical characterizations of confidentiality/secrecy, authentication/integrity, non-duplication, non-repudiation, etc.Three invited talks, by Y. Lakhnech, M. Rusinowitch, and R. Amadio, plus five submitted papers out of ten were selected for presentation at LACPV'2001. They were reviewed by the program committee consisting, besides editor, of

Hubert Comon	LSV, ENS Cachan
Mourad Debbabi	Université Laval, Québec
Jon Millen	Computer Science Lab, SRI International
Scott Stoller	State University of New York, Stony Brook

Full-size table

This volume will be published as volume 55, issue 1, in the series Electronic Notes in Theoretical Computer Science (ENTCS). This series is published electronically through the facilities of Elsevier Science B.V. and its auspices. The volumes in the ENTCS series can be accessed at the URL http://www.elsevier.nl/locate/entcsA printed version of the current volume is distributed to the participants at the workshop in Paris.We are very grateful to the following persons, whose help has been crucial for the success of LACPV'2001: Alain Finkel for his help in managing CAV satellite workshops; Mike Mislove, one of the Managing Editors of the ENTCS series, for his assistance with the use of the ENTCS style files.July 05, 2001Jean Goubault-Larrecq