Completeness and Counter-Example Generations of a Basic Protocol Logic: (Extended Abstract)

We give an axiomatic system in first-order predicate logic with equality for proving security protocols correct. Our axioms and inference rules derive the basic inference rules, which are explicitly or implicitly used in the literature of protocol logics, hence we call our axiomatic system Basic Protocol Logic (or BPL, for short). We give a formal semantics for BPL, and show the completeness theorem such that for any given query (which represents a correctness property) the query is provable iff it is true for any model. Moreover, as a corollary of our completeness proof, the decidability of provability in BPL holds for any given query. In our formal semantics we consider a “trace” any kind of sequence of primitive actions, counter-models (which are generated from an unprovable query) cannot be immediately regarded as realizable traces (i.e., attacked processes on the protocol in question). However, with the aid of Comon-Treinen's algorithm for the intruder deduction problem, we can determine whether there exists a realizable trace among formal counter-models, if any, generated by the proof-search method (used in our completeness proof). We also demonstrate that our method is useful for both proof construction and flaw analysis by using a simple example.     

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

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

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.     

Towards a Quantitative Analysis of Security Protocols

This paper contributes to further closing the gap between formal analysis and concrete implementations of security protocols by introducing a quantitative extension of the usual Dolev-Yao intruder model. This extended model provides a basis for considering protocol attacks that are possible when the intruder has a reasonable amount of computational power, in particular when he is able, with a certain probability, to guess encryption keys or other particular kind of data such as the body of a hashed message. We also show that these extensions do not augment the computational complexity of the protocol insecurity problem in the case of a finite number of interleaved protocol sessions.     

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

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

分析安全协议猜测攻击的模态逻辑方法

以CKT5逻辑为基础,对其进行了多方面重要的扩展;在原有对称密钥机制的基础上,增加了公开密钥机制和vernam加密机制以增强其描述协议的能力;打破完善加密假设,给出了一组定义和规则使主体具备猜测和验证口令的能力;给出了与在线猜测攻击相关的定理以反映在线猜测攻击的特点;通过相关引理和定理的证明,简化了猜测攻击的分析过程,使该文方法比现有方法更加简洁高效.扩展后的逻辑能够用于分析安全协议的猜测攻击,包括在线猜测攻击.     

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

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

Symbolic protocol analysis in the union of disjoint intruder theories: Combining decision procedures

Most of the decision procedures for symbolic analysis of protocols are limited to a fixed set of algebraic operators associated with a fixed intruder theory. Examples of such sets of operators comprise XOR, multiplication, abstract encryption/decryption. In this report we give an algorithm for combining decision procedures for arbitrary intruder theories with disjoint sets of operators, provided that solvability of ordered intruder constraints, a slight generalization of intruder constraints, can be decided in each theory. This is the case for most of the intruder theories for which a decision procedure has been given. In particular our result allows us to decide trace-based security properties of protocols that employ any combination of the above mentioned operators with a bounded number of sessions.     

Dolev-Yao攻击者模型的形式化描述

模型检测技术能够实现安全协议的自动化分析,是一种高效的形式化分析方法。然而,对于攻击者的建模却一直缺乏通用的方法,这导致了模型检测方法的自动化程度降低。本文为安全协议分析中,应用最为广泛的Dolev-Yao攻击者模型建立了一套形式化描述方法。遵循这一方法,可以使用任何建模语言机械地建立Dolev-Yao攻击者模型,从而大大地减少了人工分析的成份。同时,本文还使用该方法验证了两个目的完全不同的协议,证明了它的通用性。     

Dolev Yao攻击者模型的形式化描述

模型检测技术能够实现安全协议的自动化分析,是一种高效的形式化分析方法。然而,对于攻击者的建模却一直缺乏通用的方法,这导致了模型检测方法的自动化程度降低。本文为安全协议分析中,应用最为广泛的Dolev Yao攻击者模型建立了一套形式化描述方法。遵循这一方法,可以使用任何建模语言机械地建立Dolev Yao攻击者模型,从而大大地减少了人工分析的成份。同时,本文还使用该方法验证了两个目的完全不同的协议,证明了它的通用性。     

On termination problems for finitely interpreted ALGOL-like programs

Summary Main issue is: The actual termination problem for finitely interpreted non-deterministic ALGOL-like programs without procedure selfapplication and without global variables is algorithmically solvable. This result offers a new and substantial application of a theorem of Lipton: The above mentioned programs, restricted to deterministic ones, have a sound and relatively complete Hoare logic. So we conjecture: ALGOL-like programs (even non-deterministic ones with formal sharing of variables) without procedure selfapplication and without global variables have a sound and relatively complete Hoare deduction system with axioms and inference rules which reflect the syntactical structure of programs.     

Easy intruder deduction problems with homomorphisms

We present complexity results for the verification of security protocols. Since the perfect cryptography assumption is unrealistic for cryptographic primitives with visible algebraic properties, we extend the classical Dolev-Yao model by permitting the intruder to exploit these properties. More precisely, we are interested in theories such as Exclusive or and Abelian groups in combination with the homomorphism axiom. We show that the intruder deduction problem is in PTIME in both cases, improving the EXPTIME complexity results of Lafourcade, Lugiez and Treinen.     

基于时序逻辑的加密协议分析

形式化方法由于其精炼，简洁和无二义性，逐步成为分析加密协议的一条可靠和准确的途径，但是加密协议的形式化分析研究目前还不够深入，至今仍没有统一的加密协议验证体系，针对这一现状，该文从加密协议可能面临的最强大的攻击着手，提出了一种基于时序逻辑的加密协议描述方法，在该模型下，对协议行为，入侵者行为，安全需求等特性的描述均用时序逻辑公式表达，从而利用现有的统一的时空逻辑框架分析密码协议的性质，特别地，作者描述和检测了一个系统入侵者不能用任何代数和逻辑的办法获得消息的实例，通过对比，作者认为该方法具有形式化程度较高的特点。     

密码协议形式化分析的计算合理性

基于Abadi-Rowgaway的形式化加密的计算合理性定理,提出和证明了密码协议形式化分析的计算合理性定理。通过对群密钥分配协议安全性的分析,说明定理对协议的可选择攻击具有较强的分析能力,提出了群密钥分配协议的形式化方法与计算方法下安全性的形式化定义,并证明了其合理性。     

The Practice of Cryptographic Protocol Verification

We present CASRUL, a compiler for cryptographic protocols specifications. Its purpose is to verify the executability of protocols and to translate them into rewrite rules that can be used by several kinds of automatic or semi-automatic tools for finding design flaws. We also present a related complexity results concerning the protocol insecurity problem for a finite number of sessions. We show the problem is in NP without assuming bounds on messages and with non-atomic encryption keys. We also explain that in order to build an attack with a fixed number of sessions the intruder needs only to forge messages of linear size, provided that they are represented as dags.For more information: http://www.loria.fr/equipes/protheo/SOFTWARES/CASRUL/.     

密码协议形式化分析的计算合理性

基于Abadi-Rowgaway的形式化加密的计算合理性定理,论文提出和证明了密码协议形式化分析的计算合理性定理。通过对群密钥分配协议的分析,说明本文的定理对协议的可选择攻击具有较强的分析能力,论文提出了群密钥分配协议的形式化方法与计算方法下安全性的形式化定义,并证明了其合理性。     

Chosen-name Attacks: An Overlooked Class of Type-flaw Attacks

In the context of Dolev-Yao style analysis of security protocols, we consider the capability of an intruder to dynamically choose and assign names to agents. This capability has been overlooked in all significant protocol verification frameworks based on formal methods. We identify and classify new type-flaw attacks arising from this capability.Several examples of protocols that are vulnerable to this type of attack are given, including Lowe's modification of KSL. The consequences for automatic verification tools are discussed.     

Extending Security Protocol Analysis: New Challenges

We argue that formal analysis tools for security protocols are not achieving their full potential, and give only limited aid to designers of more complex modern protocols, protocols in constrained environments, and security APIs. We believe that typical assumptions such as perfect encryption can and must be relaxed, while other threats, including the partial leakage of information, must be considered if formal tools are to continue to be useful and gain widespread, real world utilisation. Using simple example protocols, we illustrate a number of attacks that are vital to avoid in security API design, but that have yet to be modelled using a formal analysis tool. We seek to extract the basic ideas behind these attacks and package them into a wish list of functionality for future research and tool development.