共识协议的形式化验证研究现状与展望

分布式系统在计算环境中发挥重要的作用,其中的共识协议算法用于保证节点间行为的一致性.共识协议的设计错误可能导致系统运行故障,严重时可能对人员和环境造成灾难性的后果,因此保证共识协议设计的正确性非常重要.形式化验证能够严格证明设计模型中目标性质的正确性,适合用于验证共识协议.然而,随着分布式系统的规模增大,问题复杂度提升,使得分布式共识协议的形式化验证更为困难.采用什么方法对共识协议的设计进行形式化验证、如何提升验证规模,是共识协议形式化验证的重要研究问题.对目前采用形式化方法验证共识协议的研究工作进行调研,总结其中提出的重要建模方法和关键验证技术,并展望该领域未来有潜力的研究方向.     

Business Processes Verification for e-Government Service Delivery

Domain experts knowledge represents a major source of information in the design and the development of user-centric and distributed service-based applications, such as those of e-government. Issues related both to the communication among domain and IT experts, and to the implementation of domain dependent requirements in service-based applications, have to be carefully considered to support both Public Administrations efficiency and citizen satisfaction. In this article, we provide as user-friendly approach toward business process assessment via formal verification. Starting from a semi-formal notation, well understood and largely used by domain experts, we provide a mapping to a formal specification in the form of a process algebra. This transformation makes possible formal and automatic verification of desired quality requirements. The approach has been already applied, with encouraging results, in the e-government domain to verify the quality of business processes related to the delivery of e-government digital services to citizens. Moreover, the approach is supported by a plug-in for the Eclipse platform permitting to have an integrated environment in which to design the process model and to assess its quality.     

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

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

A semantics for web services authentication

We consider the problem of specifying and verifying cryptographic security protocols for XML web services. The security specification WS-Security describes a range of XML security elements, such as username tokens, public-key certificates, and digital signatures, amounting to a flexible vocabulary for expressing protocols. To describe the syntax of these elements, we extend the usual XML data model with symbolic representations of cryptographic values. We use predicates on this data model to describe the semantics of security elements and of sample protocols distributed with the Microsoft WSE implementation of WS-Security. By embedding our data model within Abadi and Fournet's applied pi calculus, we formulate and prove security properties with respect to the standard Dolev–Yao threat model. Moreover, we informally discuss issues not addressed by the formal model. To the best of our knowledge, this is the first approach to the specification and verification of security protocols based on a faithful account of the XML wire format.     

Modeling and Verification of Real-Time Protocols for Broadcast Networks

A class of demand-assigned multiple-access (DAMA) protocols have been proposed for high-speed local area networks (LAN's) that offer integrated services for data, voice, video, and facsimile traffic. These protocols exploit the directionality of signal propagation and implement stringent real-time constraints to achieve collision-freedom. Correct implementation of DAMA protocols will require a very careful analysis of time-dependent interactions using a formal method. To date, most verification methods have been focused on asynchronous communication over point-to-point links.     

Formal Verification of a Distributed Computer System

Modeling distributed computer systems is known to be a challenging enterprise. Typically, distributed systems are comprised of large numbers of components whose coordination may require complex interactions. Modeling such systems more often than not leads to the nominal intractability of the resulting state space. Various formal methods have been proposed to address the modeling of coordination among distributed systems components. For the most part, however, these methods do not support formal verification mechanisms. By way of contrast, the L-automata/L-processes model supports formal verification mechanisms which in many examples can successfully circumvent state space explosion problems, and allow verification proofs to be extended to an arbitrary number of components. After reviewing L-automata/L-processes formalisms, we present here the formal specification of a fault-tolerant algorithm for a distributed computer system. We also expose the L-automata/L-processes verification of the distributed system, demonstrating how various techniques such as homomorphic reduction, induction, and linearization, can be used to overcome various problems which surface as one models large, complex systems.     

Toward secure and private service discovery anywhere anytime

With the advances in and convergence of Internet technologies, embedded computers, and wireless communication, computing devices have become part of our daily life. Hand-held devices and sensors with wireless connections create opportunities for many new nomadic applications. Service discovery is an essential component for cognitive science to discover existing network services just-in-time. Unlike many other approaches, we propose a service discovery model supporting nomadic users and services in public environments. Our model emphasizes secure and private service discovery in such environments. Location sensing is integrated for location dependent service discovery and is used to lessen service discovery network infrastructure requirements. We analyze the system performance and show our formal verification of the protocols. Our implementation shows that our model is feasible.     

Toward secure and private service discovery anywhere anytime

With the advances in and convergence of Internet technologies, embedded computers, and wireless communication, computing devices have become part of our daily life. Hand-held devices and sensors with wireless connections create opportunities for many new nomadic applications. Service discovery is an essential component for cognitive science to discover existing network services just-in-time. Unlike many other approaches, we propose a service discovery model supporting nomadic users and services in public environments. Our model emphasizes secure and private service discovery in such environments. Location sensing is integrated for location dependent service discovery and is used to lessen service discovery network infrastructure requirements. We analyze the system performance and show our formal verification of the protocols. Our implementation shows that our model is feasible.     

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

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

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

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

Formal interaction specification in public health surveillance systems using pi-calculus

This paper provides formal specification of interactions in typical public health surveillance systems involving healthcare agencies at local, state and federal levels. Although few standards exist for exchange of healthcare information, there is a general lack of formal models of the protocols involved in the interactions between the agencies. The quality of medical care provided is an end result of a well designed choreography of diverse services provided by different healthcare entities. One of the major challenges in this field appears to be explicit formal specification of such interactions. Such formal specification work is the first step leading to both design and verification of important properties of public healthcare systems. pi-calculus is a formal modeling technique for precise specification of semantics in interacting concurrent systems where mobility is involved. Two different configurations of public health surveillance systems are modelled using pi-calculus in this paper.     

Language definition-based compiler development

An important reason for developing a formal definition of a programming language is to provide guidance for implementors. At the very least, a formal definition establishes a standard of implementation correctness. Here we examine one avenue of compiler implementation based on a constructive functional language definition organized into a set of modular theories and syntax-directed rules. A modular implementation, whose structure follows that of the formal definition, is developed by a combination of hand coding and semiformal transformations that bring the definition down to the level of a program in a Pascal-like language. Program verification techniques are then used to confirm the correctness of the implementation steps.     

A formal methodology for integral security design and verification of network protocols

In this work we propose a methodology for incorporating the verification of the security properties of network protocols as a fundamental component of their design. This methodology can be separated in two main parts: context and requirements analysis along with its informal verification; and formal representation of protocols and the corresponding procedural verification. Although the procedural verification phase does not require any specific tool or approach, automated tools for model checking and/or theorem proving offer a good trade-off between effort and results. In general, any security protocol design methodology should be an iterative process addressing in each step critical contexts of increasing complexity as result of the considered protocol goals and the underlying threats. The effort required for detecting flaws is proportional to the complexity of the critical context under evaluation, and thus our methodology avoids wasting valuable system resources by analyzing simple flaws in the first stages of the design process. In this work we provide a methodology in coherence with the step-by-step goals definition and threat analysis using informal and formal procedures, being our main concern to highlight the adequacy of such a methodology for promoting trust in the accordingly implemented communication protocols. Our proposal is illustrated by its application to three communication protocols: MANA III, WEP's Shared Key Authentication and CHAT-SRP.     

Vulnerability analysis of networks to detect multiphase attacks using the actor-based language Rebeca

Increasing use of networks and their complexity make the task of security analysis more and more complicated. Accordingly, automatic verification approaches have received more attention recently. In this paper, we investigate applying of an actor-based language based on reactive objects for analyzing a network environment communicating via Transport Protocol Layer (TCP). The formal foundation of the language and available tools for model checking provide us with formal verification support. Having the model of a typical network including client and server, we show how an attacker may combine simple attacks to construct a complex multiphase attack. We use Rebeca language to model the network of hosts and its model checker to find counter-examples as violations of security of the system. Some simple attacks have been modeled in previous works in this area, here we detect these simple attacks in our model and then verify the model to find more complex attacks which may include simpler attacks as their steps. We choose Rebeca because of its powerful yet simple actor-based paradigm in modeling concurrent and distributed systems. As the real network environment is asynchronous and event-based, Rebeca can be utilized to specify and verify the asynchronous systems, including network protocols.     

一种新的安全协议形式化验证方法

形式化方法能有效检验安全协议的安全性，BAN类逻辑的发展极大地促进了这一领域的研究，但是现有的BAN类逻辑仍然存在许多问题．在分析现有BAN类逻辑的基础上，提出一种新的安全协议形式化验证方法，实现现有BAN类逻辑的验证功能，并使安全协议验证工作简单可行，便于实现机器自动验证．为安全协议形式化验证提供了一种新的途径．     

基于类pi演算的电子支付协议安全性形式化研究

设计一个满足安全需求的协议非常困难,并且极易出错,因此利用形式化方法来检验安全协议引起了人们极大的关注。使用了类pi演算来验证电子支付协议的认证性和匿名性。