Formalizing and Analyzing the Needham-Schroeder Symmetric-Key Protocol by Rewriting

This paper reports on work in progress on using rewriting techniques for the specification and the verification of communication protocols. As in Genet and Klay's approach to formalizing protocols, a rewrite system describes the steps of the protocol and an intruder's ability of decomposing and decrypting messages, and a tree automaton encodes the initial set of communication requests and an intruder's initial knowledge. In a previous work we have defined a rewriting strategy that, given a term t that represents a property of the protocol to be proved, suitably expands and reduces t using the rules in and the transitions in to derive whether or not t is recognized by an intruder. In this paper we present a formalization of the Needham-Schroeder symmetric-key protocol and use the rewriting strategy for deriving two well-known authentication attacks.     

Reachability Analysis over Term Rewriting Systems

This paper surveys some techniques and tools for achieving reachability analysis over term rewriting systems. The core of those techniques is a generic tree automata completion algorithm used to compute in an exact or approximated way the set of descendants (or reachable terms). This algorithm has been implemented in the tool. Furthermore, we show that many classes with regular sets of descendants of the literature corresponds to specific instances of the tree automata completion algorithm and can thus be efficiently computed by . An extension of the completion algorithm to conditional term rewriting systems and some applications are also presented.     

Descendants of a recognizable tree language for sets of linear monadic term rewrite rules

For a tree language L and a set S of term rewrite rules over Σ, the descendant of L for S is the set S^∗(L) of trees reachable from a tree in L by rewriting in S. For a recognizable tree language L, we study the set D(L) of descendants of L for all sets of linear monadic term rewrite rules over Σ. We show that D(L) is finite. For each tree automaton A over Σ, we can effectively construct a set {R₁,…,Rk} of linear monadic term rewrite systems over Σ such that and for any 1?i<j?k, .     

Conditional Term Graph Rewriting with Indirect Sharing

For reasons of efficiency, term rewriting is usually implemented by term graph rewriting. In term rewriting, expressions are represented as terms, whereas in term graph rewriting these are represented as directed graphs. Unlike terms, graphs allow a sharing of common subexpressions. In previous work, we have shown that conditional term graph rewriting is a sound and complete implementation for a certain class of CTRSs with strict equality, provided that a minimal structure sharing scheme is used. In this paper, we will show that this is also true for two different extensions of normal CTRSs. In contrast to the previous work, however, a non-minimal structure sharing scheme can be used. That is, the amount of sharing is increased.     

SQL注入攻击防御策略的研究

SQL注入攻击是Web应用中最常见的攻击,本文通过分析SQL注入攻击的原理,针对不同的攻击方法和不同的安全需求灵活使用多种防御策略堵住漏洞,如通过过滤或转义危险字符、使用正则表达式、使用URL重写技术等方法减少Web应用的风险。     

平行最外模式匹配*

平行最外策略是归约系统中适用范围非常广的策略,平行最外模式匹配研究适用于该策略的高效模式匹配方法．本文在生成自适应模式匹配自动机APMA的基础上,充分利用匹配失败状态的部分匹配信息,构造了平行最外模式匹配自动机POPMA．利用POPMA进行模式匹配,在维持空间开销不大的前提下,降低了朴素思想的2大时间开销．并将模式匹配和归约策略结台起来,几乎一遗扫描即可找出所有平行最外匹配子项,具有很高的时空效率．借助于POP-MA,还可以对平行最外策略进行改进．     

Test Sets for the Universal and Existential Closure of Regular Tree Languages

Finite test sets are a useful tool for deciding the membership problem for the universal closure of a given tree language, that is, for deciding whether a term has all its ground instances in the given language. A uniform test set for the universal closure must serve the following purpose: In order to decide membership of a term, it is sufficient to check whether all its test set instances belong to the underlying language. A possible application, and our main motivation, is ground reducibility, an essential concept for many approaches to inductive reasoning. Ground reducibility modulo some rewrite system is membership in the universal closure of the set of reducible ground terms. Here, test sets always exist, and several algorithmic approaches are known. The resulting sets, however, are often unnecessarily large. In this paper we consider regular languages and linear closure operators. We prove that universal as well as existential closure, defined analogously, preserve regularity. By relating test sets to tree automata and to appropriate congruence relations, we show how to characterize, how to compute, and how to minimize ground and non-ground test sets. In particular, optimal solutions now replace previous ad hoc approximations for the ground reducibility problem.     

Lifting Infinite Normal Form Definitions From Term Rewriting to Term Graph Rewriting

nfinite normal forms are a way of giving semantics to non-terminating rewrite systems. The notion is a generalization of the Böhm tree in the lambda calculus. It was first introduced in [Ariola, Z. M. and S. Blom, Cyclic lambda calculi, in: Abadi and Ito [Abadi, M. and T. Ito, editors, “Theoretical Aspects of Computer Software,” Lecture Notes in Computer Science 1281, Springer Verlag, 1997], pp. 77–106] to provide semantics for a lambda calculus on terms with letrec. In that paper infinite normal forms were defined directly on the graph rewrite system. In [Blom, S., “Term Graph Rewriting - syntax and semantics,” Ph.D. thesis, Vrije Universiteit Amsterdam (2001)] the framework was improved by defining the infinite normal form of a term graph using the infinite normal form on terms. This approach of lifting the definition makes the non-confluence problems introduced into term graph rewriting by substitution rules much easier to deal with. In this paper, we give a simplified presentation of the latter approach.     

Paramodulation and Knuth–Bendix Completion with Nontotal and Nonmonotonic Orderings

Up to now, all existing completeness results for ordered paramodulation and Knuth–Bendix completion have required term ordering to be well founded, monotonic, and total(izable) on ground terms. For several applications, these requirements are too strong, and hence weakening them has been a well-known research challenge.Here we introduce a new completeness proof technique for ordered paramodulation where the only properties required on are well-foundedness and the subterm property. The technique is a relatively simple and elegant application of some fundamental results on the termination and confluence of ground term rewrite systems (TRS).By a careful further analysis of our technique, we obtain the first Knuth–Bendix completion procedure that finds a convergent TRS for a given set of equations E and a (possibly non-totalizable) reduction ordering whenever it exists. Note that being a reduction ordering is the minimal possible requirement on , since a TRS terminates if, and only if, it is contained in a reduction ordering.     

依赖项重写系统及其在程序设计语言中的应用

面重写系统是一种简洁通用的计算模型,在许多领域中有着重要的应用。     

Infinitary Combinatory Reduction Systems

We define infinitary Combinatory Reduction Systems (iCRSs), thus providing the first notion of infinitary higher-order rewriting. The systems defined are sufficiently general that ordinary infinitary term rewriting and infinitary λ-calculus are special cases.Furthermore, we generalise a number of known results from first-order infinitary rewriting and infinitary λ-calculus to iCRSs. In particular, for fully-extended, left-linear iCRSs we prove the well-known compression property, and for orthogonal iCRSs we prove that (1) if a set of redexes U has a complete development, then all complete developments of U end in the same term and that (2) any tiling diagram involving strongly convergent reductions S and T can be completed iff at least one of S/T and T/S is strongly convergent.We also prove an ancillary result of independent interest: a set of redexes in an orthogonal iCRS has a complete development iff the set has the so-called finite jumps property.     

Smoothness of Boundaries of Regular Sets

We prove that the boundary of an r-regular set is a codimension one manifold of class C ¹.     

General Algorithms for Permutations in Equational Inference

Mechanized systems for equational inference often produce many terms that are permutations of one another. We propose to gain efficiency by dealing with such sets of terms in a uniform manner, by the use of efficient general algorithms on permutation groups. We show how permutation groups arise naturally in equational inference problems, and study some of their properties. We also study some general algorithms for processing permutations and permutation groups, and consider their application to equational reasoning and term-rewriting systems. Finally, we show how these techniques can be incorproated into resolution theorem-proving strategies.     

Mechanizing and Improving Dependency Pairs

The dependency pair technique is a powerful method for automated termination and innermost termination proofs of term rewrite systems (TRSs). For any TRS, it generates inequality constraints that have to be satisfied by well-founded orders. We improve the dependency pair technique by considerably reducing the number of constraints produced for (innermost) termination proofs. Moreover, we extend transformation techniques to manipulate dependency pairs that simplify (innermost) termination proofs significantly. To fully mechanize the approach, we show how transformations and the search for suitable orders can be mechanized efficiently. We implemented our results in the automated termination prover AProVE and evaluated them on large collections of examples. Supported by the Deutsche Forschungsgemeinschaft DFG, grant GI 274/5-1.     

高效率重写型程序的设计

本文考虑如何设计高效率(即重写步数较少的)重写型程序。文中以计算Fibonacci数列的程序为例．比较具有相同功能的重写型程序,展示编写高效率重写型程序的可能性。介绍利用动态项重写计算编写高效率重写型程序的直观、简洁的方法。其中．动态项重写计算是项重写系统的元计算模型,其计算同样基于项重写。     

Completion for Multiple Reduction Orderings

We present a completion procedure (called MKB) that works for multiple reduction orderings. Given equations and a set of reduction orderings, the procedure simulates a computation performed by the parallel processes each of which executes the standard completion procedure (KB) with one of the given orderings. To gain efficiency, however, we develop new inference rules working on objects called nodes, which are data structures consisting of a pair s : t of terms associated with the information to show which processes contain the rule s t (or t s) and which processes contain the equation s t. The idea is based on the observation that some inferences made in different processes are often closely related, so we can design inference rules that simulate these inferences all in a single operation. Our experiments show that MKB is significantly more efficient than the naive simulation of parallel execution of KB procedures, when the number of reduction orderings is large enough. We also present an extension of this technique to the unfailing completion for multiple reduction orderings, which is useful in various areas of automated reasoning, including equational theorem proving.     

必要平行最外归约策略

在必要集、必要位置等概念基础上,定义了必要平行最外归约策略．基于最小化必要集思想,该策略适用于正则系统全集,并接近按需调用策略的效率,在适用范围、效率和可实现性三个方面得到了兼顾．