基于同态的安全协议攻击及其形式化验证

介绍2种利用加密算法同态特性的安全协议攻击,定义安全协议项代数表示和基于角色行为序列的协议模型,提出一种基于角色行为实例交互的安全协议约束序列生成方法,应用等式理论将Dolev D等人提出的Dolev-Yao模型（IEEE Transactions on Information Theory,1983,第12期）进行扩展,设计攻击者一阶逻辑演绎系统,采用约束求解方法对NSL协议进行建模和形式化验证,发现基于“完美密码系统假设”无法验证的同态攻击。     

动态项重写计算

1.引言项重写系统是一种受到广泛研究和应用的形式计算模型。一个项重写系统由一组称为重写规则的定向等式组成。它的计算基于代入、匹配和替换,除具有方向性外,与等式推导一致。虽然项重写系统形式简单、计算单纯,但它同时又具有与λ计算及图灵机相同的计算能力。正是它的简洁性及计算能力使它受到广泛的研究和应用:项重写系统为抽象数据类型提供类型、为函数型语言提供操作语义、为定理自动证明提供推理工具。对于项重写系统本身也有大量的研究:如合流性、终止性、等价性等。     

基于合一替换推理的密码协议分析

提出了一种简单的，更适合于自动化操作的密码协议分析方法，通过进一步分析攻击者的计算能力，形成一个有效的自动推理系统。攻击者为应答挑战主体的消息。把该消息应答转化为利用推理系统进行合一替换。并分别给出了Needham-Schroede协议的推理说明。     

基于状态转移系统的安全协议形式模型

提出一种基于状态转移系统的安全协议模型,以Dolev-Yao攻击者模型为前提假设,以状态转移系统为框架,用语义编码的方式定义消息和事件,用重写关系定义协议规则,用事件的集合来描述协议的安全属性,并给出安全属性的检验策略。该模型能够对安全协议进行精确的形式化描述,且便于实现自动化分析。     

基于树语言逼近的安全协议形式化分析

利用形式化方法或工具自动化分析实用安全协议十分必要,定理证明技术因其可解决无限状态系统的验证备受关注,但扩展其验证规模和自动化实现时仍然存在一些局限性。以定理证明和重写逼近理论为基础,以项重写形式化定义协议模型,以树自动机模拟协议攻击者知识集,给出攻击者知识集可达项逼近求解的算法,并根据上述模型讨论秘密性和认证性的验证方法,最后以Needham-Schroeder公钥认证协议为例验证模型的有效性,并指出下一步研究方向。     

归纳法推理中的项重写策略*

本文介绍归纳法推理系统中的项重写策略．该策略根据不同的待重写项term，分别运用公理、重写引理、函数定义、项重写规则等重写项term，以期得到一个更接近推理目标的巳重写项．这一策略已在微机上用编译LlsP语言实现．     

归纳法推理中的项重写策略

本文介绍归纳法推理系统中的项重写策略，该策略根据不同的待重写项ｔｅｒｍ，分别运用公理、重写引理、函数定义、项重写规则等重写项ｔｅｒｍ，以期得到一个更接近推理目标的已重写项，这一策略已在微机上用编译ＬＩＳＰ语言实现。     

项重写系统弱基终止性的归纳证明

1.引言项重写系统是一种受到广泛研究和应用的形式计算模型。一个项重写系统由一组称为重写规则的定向等式组成。例如,下面的R是一个由五个重写规则组成的、定义用({0,s})表示的自然数集N上的两倍函数d(x)=2×n:N→N的项重写系统:     

一种基于π t演算的安全协议建模方法

安全协议模型是安全协议分析与验证的基础,现有的建模方法中存在着一些缺点,如:建模复杂、重用性差等.为此提出了一种类型化的π演算:πt演算,并给出了相应类型推理规则和求值规则,πt演算的安全性也得到了证明.πt演算可以对安全协议、协议攻击者进行形式化建模.基于πt演算的安全协议模型及其建模过程使用NRL协议为例做出了说明.同时给出了攻击者模型,并证明了基于πt演算的安全协议攻击者模型与D-Y攻击者模型在行动能力上是一致的.这保证了基于πt演算的安全协议模型的验证结果的正确性.基于πt演算的建模方法能在协议数据语义、协议参与者知识方面实现细致的描述.与同类方法相比,该方法可提供多种分析支持,具有更好的易用性、重用性.分析表明,该方法可以在建模中发现一定的安全协议漏洞.     

概念代数—新一代数据库系统的理论

念代数ＣＡ是Ｎｉｌｓｓｏｎ教授以格（ｌａｔｔｉｃｅ）理论为数学背景提出的一个新的代数系统。在ＣＡ中，关系范型、ＯＯ范型、逻辑程序设计和框架知识表示获得了统一的表示－概念项，项进一步组成句子。一个完整的知识库就由这样折的项和句子组成。推理操作是一组被称为重写规则的代数公理。目前的ＣＡ还只是个代数系统雏形，有很多方面有待扩充。本文对概念代数进行综述，并给出初步的扩充。     

Inductive proof search modulo

We present an original narrowing-based proof search method for inductive theorems in equational rewrite theories given by a rewrite system $\mathcal{R}$ and a set E of equalities. It has the specificity to be grounded on deduction modulo and to rely on narrowing to provide both induction variables and instantiation schemas. Whenever the equational rewrite system $(\mathcal{R},E)$ has good properties of termination, sufficient completeness, and when E is constructor and variable preserving, narrowing at defined-innermost positions leads to consider only unifiers which are constructor substitutions. This is especially interesting for associative and associative-commutative theories for which the general proof search system is refined. The method is shown to be sound and refutationally correct and complete. A major feature of our approach is to provide a constructive proof in deduction modulo for each successful instance of the proof search procedure.     

Structures for Abstract Rewriting

When rewriting is used to generate convergent and complete rewrite systems in order to answer the validity problem for some theories, all the rewriting theories rely on a same set of notions, properties, and methods. Rewriting techniques have been used mainly to answer the validity problem of equational theories, that is, to compute congruences. Recently, however, they have been extended in order to be applied to other algebraic structures such as preorders and orders. In this paper, we investigate an abstract form of rewriting, by following the paradigm of logical-system independency. To achieve this purpose, we provide a few simple conditions (or axioms) under which rewriting (and then the set of classical properties and methods) can be modeled, understood, studied, proven, and generalized. This enables us to extend rewriting techniques to other algebraic structures than congruences and preorders such as congruences closed under monotonicity and modus ponens. We introduce convergent rewrite systems that enable one to describe deduction procedures for their corresponding theory, and we propose a Knuth-Bendix–style completion procedure in this abstract framework.     

Maude: specification and programming in rewriting logic

Maude is a high-level language and a high-performance system supporting executable specification and declarative programming in rewriting logic. Since rewriting logic contains equational logic, Maude also supports equational specification and programming in its sublanguage of functional modules and theories. The underlying equational logic chosen for Maude is membership equational logic, that has sorts, subsorts, operator overloading, and partiality definable by membership and equality conditions. Rewriting logic is reflective, in the sense of being able to express its own metalevel at the object level. Reflection is systematically exploited in Maude endowing the language with powerful metaprogramming capabilities, including both user-definable module operations and declarative strategies to guide the deduction process. This paper explains and illustrates with examples the main concepts of Maude's language design, including its underlying logic, functional, system and object-oriented modules, as well as parameterized modules, theories, and views. We also explain how Maude supports reflection, metaprogramming and internal strategies. The paper outlines the principles underlying the Maude system implementation, including its semicompilation techniques. We conclude with some remarks about applications, work on a formal environment for Maude, and a mobile language extension of Maude.     

A class of confluent term rewriting systems and unification

The narrowing mechanism and term rewriting systems are powerful tools for constructing complete and efficient unification algorithms for useful classes of equational theories. This has been shown for the case where term rewriting systems are confluent and noetherian (i.e., terminating). In this paper we show that the narrowing mechanism, combined with ordinary unification, yields a complete unification algorithm for equational theories that can be described by a closed linear term rewriting system with the non-repetition property; this class allows non-terminating rewrite systems. For some special forms of input terms, narrowing generates complete sets of E-unifiers without resorting to the non-repetition property. The key observation underlying the proof is that a reduction sequence in this class of term rewriting system can be transformed into one which possesses properties that enable a completeness proof.     

Proving operational termination of membership equational programs

Reasoning about the termination of equational programs in sophisticated equational languages such as Elan, Maude, OBJ, CafeOBJ, Haskell, and so on, requires support for advanced features such as evaluation strategies, rewriting modulo, use of extra variables in conditions, partiality, and expressive type systems (possibly including polymorphism and higher-order). However, many of those features are, at best, only partially supported by current term rewriting termination tools (for instance mu-term, C i ME, AProVE, TTT, Termptation, etc.) while they may be essential to ensure termination. We present a sequence of theory transformations that can be used to bridge the gap between expressive membership equational programs and such termination tools, and prove the correctness of such transformations. We also discuss a prototype tool performing the transformations on Maude equational programs and sending the resulting transformed theories to some of the aforementioned standard termination tools.     

External Rewriting for Skeptical Proof Assistants

This paper presents the design, the implementation, and experiments of the integration of syntactic, conditional possibly associative-commutative term rewriting into proof assistants based on constructive type theory. Our approach is called external because it consists in performing term rewriting in a specific and efficient environment and checking the computations later in a proof assistant. Two typical systems are considered in this work: ELAN, based on the rewriting calculus, as the term rewriting-based environment, and Coq, based on the calculus of inductive constructions as the proof assistant. We first formalize the proof terms for deduction by rewriting and strategies in ELAN using the rewriting calculus with explicit substitutions. We then show how these proof terms can soundly be translated into Coq syntax where they can be directly type checked. For the method to be applicable for rewriting modulo associativity and commutativity, we provide an effective method to prove equalities modulo these axioms in Coq using ELAN. These results have been integrated into an ELAN-based rewriting tactic in Coq.     

A Local Graph-rewriting System for Deciding Equality in Sum-product Theories

In this paper we give a graph-based decision procedure for a calculus with sum and product types. Although our motivation comes from the Bird-Meertens approach to reasoning algebraically about functional programs, the language used here can be seen as the internal language of a category with binary products and coproducts. As such, the decision procedure presented has independent interest.A standard approach based on term rewriting would work modulo a set of equations; the present work proposes a simpler approach, based on graph-rewriting. We show in turn how the system covers reflection equational laws, fusion laws, and cancellation laws.