一种改进的密码协议形式化模型

多重集重写MSR(multiset rewriting)模型是一种基于多重集重写的协议形式化建模方法.从目前的研究成果来看,该模型并不完善.针对其攻击者模型验证协议存在的不足,对MSR模型进行了改进,并给出了基于MSR模型的秘密性和认证性描述.实践表明,对模型的改进进一步完善了原模型.     

无人机无线通信协议的形式化认证分析与验证

针对无人机组与地面控制站之间进行无线通信时的身份认证问题,首先分析无线通信协议的工作流程及其形式化表示,然后对网络系统中的诚实主体和攻击者进行形式化建模,其中推导了协议安全属性的LTL公式,通过建立密钥机制,实现控制站与无人机节点以及各个无人机节点之间的身份认证;运用模型检测工具SPIN验证无线通信协议的一致性,其中提出一种改进的知识项获取方法,加快攻击者需掌握知识集的求取过程;验证结果表明该无人机无线通信协议具有中间人攻击漏洞。     

安全协议认证的形式化方法研究

安全协议认证是网络安全领域中重大课题之一。形式化方法多种多样。该文首先论述了模型检测技术及其在安全协议验证中的应用,然后介绍了各种定理证明方法和定理证明工具,接着讨论其它形式化验证方法,最后论述形式化方法的一些研究方向。     

基于 Spin/Promela 的 Woo-Lam 协议安全性质高效验证磁

形式化方法是分析验证安全协议的重要技术之一。模型检测是用在形式化方法中实现形式化自动验证的重要手段。基于 Promela 语言,将 P ．Maggi 和 R ．Sisto 提出的建模方法扩展到建立包含三个合法主体和一个攻击者的复杂模型,枚举法和打表法同时被运用在求解攻击者模型需要表示的知识项过程中,提高了协议建模效率,保证了建模准确性。以Woo-Lam 协议为例,运用 Spin 工具成功发现一个已知著名攻击。此通用方法适用于类似复杂协议形式化分析与验证。     

IEEE 802.11i 协议的形式化分析

Furqan提出运用串空间理论对IEEE 802.11i协议进行形式化验证的基础上,对IEEE 802.11i 协议的串空间模型进行了改进,并证明了Furqan没有证明的保密性以及服务器的认证性。分析结果证明,在目前的攻击者模型中,IEEE 802.11i 协议是安全的。     

基于连续ARQ协议的隐蔽洪水攻击

通信协议设计时的疏漏很容易造成严重的后果,因此有必要采用形式化的方法来保证协议的安全性和可靠性.模型检测是一种具有工业应用前景的形式化分析方法,并具有很高的自动化程度,适合于协议的分析与验证.文中采用模型检测工具SPIN对连续ARQ协议建模,通过验证该协议的基本属性证明所建模型的正确性.然后依据Dolev和Yao的思想加入攻击者模型再进行分析,发现了连续ARQ协议的一个新漏洞,攻击者能够利用这个漏洞造成大量冗余数据的传输和存储.这种攻击建立在互信的数据传输基础上,且攻击者并不直接发送冗余数据,因此具有很高的隐蔽性.     

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

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

一种基于模重写系统的攻击者推理方法

为了解决安全协议验证中攻击者模等式理论推理的可操作性问题,提出并设计了一种基于模重写系统的攻击者推理方法。该方法建立在一个反映两种密码原语代数特性的联合理论实例之上,由一组定向的重写规则和非定向的等式构成,前者进一步转化为项重写系统TRS(Term Rewriting System),而后者则转化为有限等价类理论,通过定义项间的模重写关系,使二者构成一个可以反映攻击者针对联合理论代数项操作能力的模重写系统。实例分析表明,该模型为攻击者模等式推理规则赋予了明确的操作语义,可以使攻击者达到对安全协议代数项规约、推理的目的。     

802.11i双向认证协议的模型检查

确保安全协议的正确性对于保证Internet上安全敏感的业务非常重要。采用形式化方法建模和验证安全协议可以检测到传统测试手段难以发现的错误。模型检查作为形式化验证方法的一种,有着自动化和提供反例等诸多优点。使用模型检查工具SPIN对802.11i双向认证协议EAP-TLS进行验证,提取出包含协议设计重要细节的形式化模型,对协议安全属性采用线性时态逻辑抽象,并验证协议模型是否满足安全属性。提出了一种使用PROMELA建模认证协议的方法。     

基于串空间的可信计算协议分析

可信计算技术能为终端、网络以及云计算平台等环境提供安全支撑,其本身的安全机制或者协议应该得到严格的形式化证明.该文基于串空间模型对其远程证明协议进行了分析.首先,扩展了串空间的消息代数和攻击者串,使其能表达可信计算相关的密码学操作,并对衍生的定理进行了证明;并且提出了4个新的认证测试准则,能对协议中的加密、签名、身份生成和哈希等组件进行推理.其次,基于扩展的串空间模型对远程证明协议的安全属性(隐私性、机密性和认证性)进行了抽象和分析.最后,给出了对发现攻击的消息流程,并基于ARM开发板对其中的布谷鸟攻击进行了实现,验证了串空间的分析结果.     

电力智能单元传输规约安全性分析模型研究

电力智能单元传输规约的安全性是保障智能电网中智能通信实现高速、可靠、安全的基础。为了构建适用于电力智能单元传输规约的安全性分析模型,概述了主流的协议安全性分析理论与方法。基于符号模型的形式化方法包括逻辑推理、模型检验、定理证明;基于计算模型的计算方法包括RO模型、BCP模型、CK模型以及UC模型;基于计算可靠性理论的方法包括映射方法、模型方法、形式化方法的计算可靠性以及计算方法的直接形式化。提出了面向智能电网领域的电力智能单元传输规约安全性分析模型,为进一步的电力智能化单元传输规约的安全性分析奠定了基础。     

基于事件逻辑的改进Needham-Schroeder协议安全性证明

安全协议是现代网络安全的基础,密码协议的安全性证明是一个挑战性的问题。事件逻辑是一种描述分布式系统中状态迁移的形式化方法,用于刻画安全协议的形式化描述,是定理证明的基础。用事件序语言、事件类和一个表示随机数、密钥、签名和密文的原子类,给出身份认证协议可以被形式化定义和强认证性证明理论。利用该理论对增加时间戳的Needham-Schroeder协议安全性进行证明,证明改进的Needham-Schroeder协议是安全的。此理论适用于类似复杂协议形式化分析与验证。     

Mechanizing Weakly Ground Termination Proving of Term Rewriting Systems by Structural and Cover-Set Inductions

The paper presents three formal proving methods for generalized weakly ground terminating property, i.e., weakly terminating property in a restricted domain of a term rewriting system, one with structural induction, one with cover-set induction, and the third without induction, and describes their mechanization based on a meta-computation model for term rewriting systems-dynamic term rewriting calculus. The methods can be applied to non-terminating, non-confluent and/or non-left-linear term rewriting systems. They can do "forward proving" by applying propositions in the proof, as well as "backward proving" by discovering lemmas during the proof.     

密码协议安全性证明系统解析器的设计与实现*

可证明安全性是密码协议安全性评估的重要依据,但手写安全性证明容易出错且正确性难以判定,利用计算机辅助构造游戏序列进而实现自动化证明是当前一种可行的方法。为此提出一种基于进程演算的密码协议形式化描述模型,定义了描述密码协议安全性证明中攻击游戏的语法规则,并借助工具LEX和YACC,设计出解析器程序,将密码协议及其安全性的形式化描述解析为自动化安全性证明系统的初始数据结构,并用实例来说明这种方法的可行性。     

Security protocols: from linear to classical logic by abstract interpretation

We relate two models of security protocols, namely the linear logic or multiset rewriting model, and the classical logic, Horn clause representation of protocols. More specifically, we show that the latter model is an abstraction of the former, in which the number of repetitions of each fact is forgotten. This result formally characterizes the approximations made by the classical logic model.     

Term rewriting and its application to recognizing handwritten Hindu numerals

In this paper the theoretical basis is presented and the implementation of a term rewriting system based on algebraic specifications is described. The input to this system is represented by an algebraic specification language, which forms not only the set of axioms but also the sorts, variables, operators and terms of a specific simulated theory or application. Rewriting and matching mechanisms provide the formal methodology for evaluating terms and proving assertions in an algebraic theory. Specifications are evaluated by interpreting terms by means of rewrite rules. The rules are described by the axioms of the specifications where the finite termination and congruence properties are assumed. A term rewriting system to recognize handwritten Hindu numerals is introduced as a case study. Besides rewriting, a robust algorithm is proposed to segment the numeral's image into strokes based on feature points and to identify cavity features. A syntactic representation (term) of the input image is matched and rewritten against a set of rules. Experimental results proved that the proposed system is tolerant to recognize a variety of numeral shapes with 96% successful recognition rate.     

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.     

A Categorical Critical-pair Completion Algorithm

We introduce a general critical-pair/completion algorithm, formulated in the language of category theory. It encompasses the Knuth–Bendix procedure for term rewriting systems (also modulo equivalence relations), the Gröbner basis algorithm for polynomial ideal theory, and the resolution procedure for automated theorem proving. We show how these three procedures fit in the general algorithm, and how our approach relates to other categorical modeling approaches to these algorithms, especially term rewriting.