Verifying security protocols with PVS: widening the rank function approach

To enable the verification of authentication protocols, Schneider formulated the rank function approach which could be used, under suitable circumstances, to verify protocols modelled using the process algebra CSP. We develop this theoretical result and extend it to a practical framework which can be used to model and analyse a wider variety of security protocols with respect to a wider range of security specifications than were hitherto possible. These results are achieved using PVS, which also provides tool support for the rank function approach.     

Verifying programs in the calculus of inductive constructions

This paper deals with a particular approach to the verification of functional programs. A specification of a program can be represented by a logical formula [Con86, NPS90]. In a constructive framework, developing a program then corresponds to proving this formula. Given a specification and a program, we focus on reconstructing a proof of the specification whose algorithmic contents corresponds to the given program. The best we can hope is to generate proof obligations on atomic parts of the program corresponding to logical properties to be verified. First, this paper studies a weak extraction of a program from a proof that keeps track of intermediate specifications. From such a program, we prove the determinism of retrieving proof obligations. Then, heuristic methods are proposed for retrieving the proof from a natural program containing only partial annotations. Finally, the implementation of this method as a tactic of theCoq proof assistant is presented.This research was partly supported by ESPRIT Basic Research Action Types for Proofs and Programs and by Programme de Recherche Coordonnes and CNRS Groupement de Recherche Programmation.     

Verifying authentication protocols in CSP

This paper presents a general approach for analysis and verification of authentication properties using the theory of Communicating Sequential Processes (CSP). The paper aims to develop a specific theory appropriate to the analysis of authentication protocols, built on top of the general CSP semantic framework. This approach aims to combine the ability to express such protocols in a natural and precise way with the ability to reason formally about the properties they exhibit. The theory is illustrated by an examination of the Needham-Schroeder (1978) public key protocol. The protocol is first examined with respect to a single run and then more generally with respect to multiple concurrent runs     

Verifying conformance of multi-agent commitment-based protocols

Although several approaches have been proposed to specify multi-agent commitment-based protocols that capture flexible and rich interactions among autonomous and heterogeneous agents, very few of them synthesize their formal specification and automatic verification in an integrated framework. In this paper, we present a new logic-based language to specify commitment-based protocols, which is derived from ACTL^1c, a logic extending CTL¹ with modalities to represent and reason about social commitments and their actions. We present a reduction technique that formally transforms the problem of model checking ACTL^1c to the problem of model checking GCTL¹ (an extension of CTL¹ with action formulae). We prove that the reduction technique is sound and we fully implement it on top of the CWB-NC model checker to automatically verify the NetBill protocol, a motivated and specified example in the proposed specification language. We also apply the proposed technique to check the compliance of another protocol: the Contract Net protocol with given properties and report and discuss the obtained results. We finally develop a new symbolic algorithm to perform model checking dedicated to the proposed logic.     

Efficient verification of security protocols using partial-order reductions

In this paper we explore how partial-order reduction can make the task of verifying security protocols more efficient. These reduction techniques have been implemented in our tool Brutus. Partial-order reductions have proved very useful in the domain of model checking reactive systems. These reductions are not directly applicable in our context because of additional complications caused by tracking knowledge of various agents. We present partial-order reductions in the context of verifying security protocols and prove their correctness. Experimental results demonstrating the effectiveness of this reduction technique are also presented. Published online: 24 January 2003     

一种基于关联规则的安全协议验证方法

提出了一种基于关联规则的安全协议形式化分析方法。从主体认证关联、消息间关联和消息内部关联三个角度去刻画协议,提出了基于以上关联特点的协议验证方法。利用该方法对Woo and Lam认证协议进行了逆向验证分析,成功推导出现有的已知攻击路径,使这些已知攻击路径的推导能统一于该验证方法;同时还发现了一个未知的攻击路径,为协议的形式化分析提供了新思路。     

一种适于带时间戳安全协议的形式化分析方法

提出了一种适用于带有时间戳的安全协议的有色Petri（CPN）形式化分析方法,利用一个非自动时钟来描述协议中涉及的时间因素。对著名的WMF协议建模,利用CPN Tools,采用CPN ML语言编写查询函数验证协议的新鲜性,从而发现协议的漏洞。应用分析结果表明该方法有效,且操作简单容易理解。     

Verifying the summit bus converter protocols with symbolic model checking

We report on our investigation of a new verification tool, the Symbolic Model Verifier (SMV), created at Carnegie Mellon University. We have successfully, employed this tool to detect deadlock in an industrial design, namely, Hewlett-Packard's Summit bus converter chips. In addition to locating a known deadlock in the original chip design and checking its solution, we successfully detected other previously unknown defects in the design. In our experiments, we were able to verify properties on finite-state models of the circuit with 150 to 200 state variables in a matter of minutes.     

Safely composing security protocols

Security protocols are small programs that are executed in hostile environments. Many results and tools have been developed to formally analyze the security of a protocol in the presence of an active attacker that may block, intercept and send new messages. However even when a protocol has been proved secure, there is absolutely no guarantee if the protocol is executed in an environment where other protocols are executed, possibly sharing some common keys like public keys or long-term symmetric keys. In this paper, we show that security of protocols can be easily composed. More precisely, we show that whenever a protocol is secure, it remains secure even in an environment where arbitrary protocols satisfying a reasonable (syntactic) condition are executed. This result holds for a large class of security properties that encompasses secrecy and various formulations of authentication. This work has been partly supported by the RNTL project POSé and the ARA SSIA Formacrypt.     

安全协议的测试与证明

提出通过测试来证明安全协议的方法。以NS和NSL协议为例,首先将协议形式化为事件序列,协议的性质可以表示为序列上的性质。协议的完整运行可以系统地生成,因此,协议的性质可以系统地测试。形式化和测试在函数程序设计语言Haskell中完成。     

安全协议的规范化设计

提出运用组合方法进行安全协议设计。给出了协议中基件与组件的定义,根据组件的安全属性设计实现相应安全目标的单步协议;定义组合规则,确保不同的单步协议能够组合成为一个复合协议,同时各个单步协议还能实现各自的安全目标。根据具体的应用背景选择合适的单步协议,按照组合规则组合后可得到满足需求的安全协议。该组合方法可将一个复合协议分解为若干基于组件的简单单步协议,使得协议的设计与分析易于实现。     

On the secure implementation of security protocols

We consider the problem of implementing a security protocol in such a manner that secrecy of sensitive data is not jeopardized. Implementation is assumed to take place in the context of an API that provides standard cryptography and communication services. Given a dependency specification, stating how API methods can produce and consume secret information, we propose an information flow property based on the idea of invariance under perturbation, relating observable changes in output to corresponding changes in input. Besides the information flow condition itself, the main contributions of the paper are results relating the admissibility property to a direct flow property in the special case of programs which branch on secrets only in cases permitted by the dependency rules. These results are used to derive an unwinding theorem, reducing a behavioural correctness check (strong bisimulation) to an invariant.     

On the security of fair non-repudiation protocols

We analyzed two non-repudiation protocols and found some new attacks on the fairness and termination property of these protocols. Our attacks are enabled by several inherent design weaknesses, which also apply to other non-repudiation protocols. To prevent these attacks, we propose generic countermeasures that considerably strengthen the design and implementation of non-repudiation protocols. The application of these countermeasures is finally shown by our construction of a new fair non-repudiation protocol.     

一种基于虚拟组织的网格安全协议形式化验证方法

虚拟组织是网格计算的基本管理单元,而协同计算组是虚拟组织形成的基础。对应于网格计算的复杂性,网格安全协议的分析与证明十分复杂。通过引入网格计算信道的概念,在传统Strand Space理论的基础上提出了一种基于虚拟组织的网格安全协议形式化验证方法,实现了网格环境下多用户协同计算安全协议的分析与证明。     

Information based reasoning about security protocols

We propose a notion of information based abstraction for the logical study of security protocols and study how protocol actions update agents' information. We show that interesting security properties of Needham-Schroeder like protocols can be verified automatically.     

An Attack-Finding Algorithm for Security Protocols

This paper proposes an automatic attack construction algorithm in order to find potential attacks on ecurity protocols.It is based on a dynamic strand space model,which enhances the original strand space model by introducing active nodes on strands so as to characterize the dynamic procedure of protocol execution.With exact causal dependency relations between messages considered in the model,this algorithm can avoid state space explo-sion caused by asynchronous composition.In order to get a finite state space,a new method called strand-added on demand is exploited,which extends a bundle in an incremental manner without requiring explicit configuration of protocol execution parameters.A finer granularity model of term structure is also introduced, in which subterms are divided into check subterms and data subterms .Moreover,data subterms can be further classified based on the compatible data subterm relation to obtain automatically the finite set of valid acceptable terms for an honest principal.In this algorithm,terms core is designed to represent the intruder‘s knowledge compactly,and forward search technology is used to simulate attack patterns easily.Using this algorithm,a new attack on the Dolve-Yao protocol can be found,which is even more harmful beeause the secret is revealed before the session terminates.     

Invariant-based reasoning about parameterized security protocols

We explore the applicability of the programming method of Feijen and van Gasteren to the domain of security protocols. This method addresses the derivation of concurrent programs from a formal specification, and it is based on common notions like invariants and pre- and post-conditions. We show that fundamental security concepts like secrecy and authentication can nicely be specified in this way. Using some small extensions, the style of formal reasoning from this method can be applied to the security domain. To demonstrate our approach, we discuss an authentication protocol and a public-key distribution protocol, and we deal with their composition. By focussing on a general setting where agents run the protocols multiple times, the nonce concept turns out to pop-up naturally. Although this work does not contain any new protocols, it does offer a new view on reasoning about security protocols.     

RFID安全认证协议综述

在物联网发展中,RFID技术以其轻量化的优势在物联网体系中占据重要地位。同时,RFID安全认证协议也因物理条件限制受到安全威胁。首先,通过对现行主流RFID安全认证协议进行梳理,按加密算法的量级将其划分为超轻量级、轻量级、中量级和重量级安全认证协议;然后,对其中典型的安全认证协议存在的安全问题进行分析,对近年来提出的改进协议安全性能及性能指标按量级进行讨论比较;最后,探讨了RFID安全认证协议可能的发展方向。