CCITT X.509协议的形式化分析及其改进

串空间模型是一种新兴的密码协议形式化分析工具,基于串空间模型的协议认证分析方法是比较常用的验证方法。概述了串空间模型理论和基于串空间模型的认证测试理论,并利用此理论对CCITT X.509协议进行了形式化的分析。该协议存在缺陷并对此进行了改进。     

JFK协议的安全性分析

重新定义了串空间理想概念，并扩展了有关命题和定理，从而使串空间理论能分析包含丰富密码原语的安全协议，进一步应用此扩展串空间理论分析JFK协议（一个新提出的IPsec密钥交换协议）的桉心安全属性：秘密性和认证性．通过分析证明了JFK协议的密钥和认证安全性，对JFK的分析也为扩展串空间理论的广泛应用打下了一个坚实的基础．     

Yahalom-Paulson协议的串空间模型与分析

串空间模型是一种新兴的密码协议形式化分析工具,其理论中理想和诚实概念的提出大大减少了协议的证明步骤。首次利用串空间理论从机密性和认证性两个方面对Yahalom-Paulson协议进行了分析。分析结果证明该协议是安全的。     

基于串空间的移动自组网路由协议安全性分析

为了研究Adhoc移动网络路由协议安全性的分析方法,采用串空间理论对Adhoc移动网络路由协议的安全目标进行了形式化描述,提出了Adhoc移动网络路由协议的形式化分析方法,并采用该方法对安全路由协议SRP的安全性进行验证,结果发现了安全路由协议SRP的一个安全漏洞,说明采用串空间理论对Adhoc移动网络路由协议安全性进行分析是有效的。     

基于串空间理论的kerberos协议的安全性分析

运用串空间这一前沿的安全协议形式化分析方法,对kerberos协议的安全性进行了分析,得出了协议满足认证性和机密性的结论,并给出了一种新的kerberos协议的形式化证明方法,扩展了串空间理论在实用协议分析方面的应用。     

NSSK协议的串空间模型及分析

本文介绍了串空间模型中的基本概念和定理,并首次利用串空间理论,从机密性和认证性两个方面,对改进的NSSK协议进行了分析.分析结果表明改进的NSSK协议是安全的.     

基于串空间模型安全协议形式化分析方法的研究

从串空间模型理论人手,提出了三种典型的串空间形式化方法（基于极小元理论的串空间方法、基于理想与诚实理论的串空间方法、基于认证测试理论的串空间方法）,并对每一种方法的证明步骤及优缺点进行了分析。在此基础上,应用提出的串空间方法对Yahalom协议的秘密性和认证性进行了分析。分析结果表明利用不同方法的优点,能更好地保证安全协议形式化分析的准确性。     

改进型Helsinki协议的串空间模型分析

Helsinki协议是ISO/IEC DIS 11770-3 中提出的重要认证协议,由于协议受到来自内部的攻击,Mithcell-Yeun对其进行了改进.但改进后协议的安全性仍未得到确认,为了验证改进协议是否满足其安全目标,利用串空间模型对协议进行了建模和分析.通过分析极小元所在串与其它串的关系说明协议的一致性,通过对理想的分析说明协议的保密性.结果表明改进型协议满足其安全要求,原协议存在安全缺陷的原因是最小元可能存在M1串上,这为 Mithcell-Yeun的改进提供了理论的证明与依据.     

Neuman-Stubblebine协议的串空间模型及分析

串空间模型是一种新兴的密码协议形式化分析工具,其理论中理想和诚实概念的提出大大减少了协议的证明步骤.首次利用串空间理论从机密性和认证性两个方面对Neuman-Stubblebine协议进行了分析.分析结果证明该协议是安全的,而且理想对公开密钥算法和对称密钥算法产生的协议的分析都是有效的.     

基于串空间和状态转换的认证协议分析方法

串空间是一种新兴的安全协议形式化分析模型。串空间模型中的理论证明方法虽然严谨，但难度很大。本文基于串空间模型，首先定义系统状态，并以Needham-Schroeder-Lowe公钥认证协议为例说明系统状态转换的分析过程。通过对状态转换过程中现实的跟踪考察，得出了有意义的结论。结合串空间模型，验证了该认证协议的安全性。这种分析认证协议的新方法简洁和高效，并易于实现自动化。     

Design of a class of nonlinear consensus protocols for multi‐agent systems

This paper investigates the consensus problem for multi‐agent systems and presents a class of nonlinear consensus protocols. First, we reveal some structure property of the corresponding Laplacian matrix by decomposing the interaction graph into strongly connected components. Then, by means of the input‐to‐state stability and algebraic graph theory, we propose a framework to prove consensus for multi‐agent systems with nonlinear protocols. In particular, we prove that consensus can be always reached in systems of single‐integrator agents with a directed communication topology containing a spanning tree, provided the nonlinear protocol is an odd and increasing function. The nonlinear consensus protocols proposed in this paper include the classical linear consensus protocol as a special case, and may have a wide range of applications, including consensus with faster convergence rates and with bounded control inputs. Copyright © 2012 John Wiley & Sons, Ltd.     

无速度输入多智能体系统的一致性

本文研究了有无引导者的多智能体系统在非线性协议下的一致性问题.当智能体速度信息无法获知时,分别针对有无引导者的多智能体系统设计了包含辅助系统和智能体相对位移信息的非线性分布式协议.借助图论、Lyapunov稳定性理论、Barbalat引理等方法,推导出有无引导者的多智能体系统在连通无向通讯网络中实现一致的充分条件,其次,设计了一种新的能使引导–追随者多智能体系统在有向通讯网络中实现期望一致的协议.最后,数值仿真验证了结果的正确性.     

Finite-time consensus for multi-agent systems via nonlinear control protocols

This paper investigates the fnite-time consensus problem of multi-agent systems with single and double integrator dynamics,respectively.Some novel nonlinear protocols are constructed for frst-order and second-order leader-follower multi-agent systems,respectively.Based on the fnite-time control technique,the graph theory and Lyapunov direct method,some theoretical results are proposed to ensure that the states of all the follower agents can converge to its leader agent s state in fnite time.Finally,some simulation results are presented to illustrate the efectiveness of our theoretical results.     

Robust containment of uncertain linear multi‐agent systems under adaptive protocols

In this paper, robust containment problem is investigated for a class of multi‐leader multi‐agent linear systems in the presence of time‐varying uncertainties. To achieve containment, a new kind of adaptive containment protocols are proposed for the multi‐agent systems. Specifically, the designed protocols consist of a continuous linear term and a discontinuous term. The linear term of the designed protocol is employed to achieve containment while the discontinuous term is utilized to eliminate the effect of uncertain dynamics on the achievement of containment. By using tools from non‐smooth analysis and algebraic graph theory, some efficient criteria for achieving robust containment in the closed‐loop multi‐agent systems are obtained and analyzed. One favorable property of the designed protocol is that containment in the closed‐loop multi‐agent systems can be achieved in a fully distributed fashion over any given connected and detail‐balanced communication graph without using any global information about the communication graph. The effectiveness of the analytical results is finally verified by performing numerical simulations. Copyright © 2016 John Wiley & Sons, Ltd.     

Event‐triggered Control for Cluster Consensus in Multi‐agent Networks

This paper considers the issue of cluster consensus for multiple agents in fixed and undirected networks. Agents in a network are supposed to split into several clusters, and a fraction of the agents in each cluster are pinned by virtual leaders. According to the Lyapunov stability theory and graph theory, some appropriate event‐triggered protocols are developed for consensus of the agents belonging to the same cluster, which can greatly reduce both the number of communication updates and that of control actuation updates. Finally, a numerical example is shown to demonstrate the effectiveness of the proposed theoretical results.     

认证协议的必要条件证明

提出绑定项理论并用该理论构建认证协议的必要条件定理,使用串空间理论证明该定理和3个典型认证协议。该理论能够迅速、有效地判定有缺陷的认证协议的认证属性,除了能够对认证协议的新鲜性、主体进行判定外,还能够对具有类型攻击缺陷的认证协议进行判定,为认证协议的安全判定提供一种简单、有效的理论方法。     

基于理想的协议安全性分析

1998年,Guttman等人提出了串空间理论作为一种新的密码协议形式化分析的工具.并在1999年第1次引入了关于消息代数上的理想以及诚实的概念来分析协议的保密性.由于理想结构的特殊性使得它可以刻画协议运行中消息之间的关系.利用理想的结构来分析协议的一些安全性质,例如保密性、认证性、零知识性以及如何抵抗猜测攻击.     

Iterative learning approaches to design finite-time consensus protocols for multi-agent systems

In this paper, the finite-time output consensus problem of multi-agent systems is considered by using the iterative learning control (ILC) approach. Two classes of distributed protocols are constructed from the two-dimensional system point of view (with time step and iteration number as independent variables), and are termed as iterative learning protocols. If learning gains are chosen appropriately, then all agents in a directed graph can be enabled to achieve finite-time consensus with the iterative learning protocols. Moreover, all agents in a directed graph can be guaranteed to reach finite-time consensus at any desired terminal output if the iterative learning protocols are improved by introducing the desired terminal output to some (not necessarily all) of the agents. Simulation results are finally presented to illustrate the performance and effectiveness of our iterative learning protocols.     

基于图元的事件图生成算法

与单轮运行情形不同，多轮并发运行的密码协议存在更为复杂的安全性问题。并发运行密码协议的形式化分析对象包括密码协议的多轮并发运行和多个密码协议的并发运行两种情形，且二者具有统一的形式化模型。基于扩展的串空间模型和Spi演算理论，提出用于并发运行密码协议安全属性验证的事件图模型。图元是事件图的构造单元，它满足消息事件之间的通信关系和前驱关系约束以及消息语句的新鲜性约束。定义消息事件之间、图元之间以及消息事件和图元之间的前缀、组合和选择运算，并给出事件图生成算法。     

Leader-following consensus of stochastic dynamical multi-agent systems with fixed and switching topologies under proportional-integral protocols

With the rapid development of swarm intelligence, consensus problem for multi-agent systems (MASs) has attracted substantial attention. To deal with the leader-following consensus problems in stochastic dynamical MASs with fixed and switching topologies, this article designed proportional-integral (PI) control protocols. On the basis of algebraic graph theory and stochastic analysis techniques, by selecting appropriate Lyapunov functions, it is theoretically shown that leader-following consensus of MASs with stochastic dynamics underlying fixed and switching topologies can be achieved in mean square, respectively. Sufficient criteria are derived for selecting the PI control gains. Finally, the theoretical results are illustrated through several numerical simulations.