基于STAMP的形式化安全性分析

传统的安全性分析方法用于分析由失效引起的事故能够起到很好的作用,但是目前大多数事故是由于部件间异常的交互引起的,应用传统的分析方法已经力不从心了。因此给出基于STAMP(System-Theoretic Accident Modeling and Process)的形式化安全性分析方法。首先介绍基于STAMP的安全性分析原理及分析步骤,形式化分析工具NuSMV及CTL语言;然后提出应用形式化方法进行基于STAMP的安全性分析的方法;最后,结合温控系统对方法进行了实例验证。     

认证协议的有向图模型及其安全性分析

认证协议的形式化描述及其安全性分析是安全协议形式化分析的关键问题之一.为了解决以往分析方法中协议规范形式化描述存在的问题,提出了一种协议规范有向图描述方法,并在此基础上提出了协议消息构造的逆向搜索算法.用该算法分析Woo-Lam认证协议,找到了该协议一种新的攻击方法及其攻击路径.     

基于制丝生产单元的智能调度模型研究与应用

随着智能制造理念在烟草制造行业的普及,本文针对红河烟厂的实际生产情况进行研究,对烟草制丝生产流程中的关键生产单元——烟片预处理生产单元的调度排产进行研究,将其抽象成为求解流程型有限缓冲区的流水线调度问题,通过模拟退火算法优化的遗传算法求解最优解,最后通过模拟不同规模的订单调度过程,验证了经过调度后的结果比未经过调度的结果更优,从而体现了模型的实用性。     

基于层次的智能告警关联分析模型研究

入侵检测系统的广泛使用产生了许多告警信息流,这些告警事件信息流基本上都是基于低层的攻击步骤检测,且具有较大的误告警率;各种分布式攻击进一步加剧了入侵检测系统告警事件信息流的复杂性。研究介绍了关联分析的基本原因、关联分析的基本概念,然后提出智能化入侵检测关联分析层次模型。该模型从误告警验证和抑制,到一个攻击一个告警,再到一个攻击过程对应一个场景刻画,形成一个层次。在不同的层次上,防御者对攻击的视图越来越清晰,从而为响应措施提供了精确的决策依据,进一步提高了整个入侵检测系统的智能性和可用性。     

基于扩展SysML活动图的嵌入式系统设计安全性验证方法研究

能源、交通等领域中复杂嵌入式系统设计的安全性分析与验证工作已经成为当前的重要研究热点之一;本文提出一种结合MARTE语义信息的扩展Sys ML活动图模型,用于描述安全关键应用中的嵌入式系统动态行为的设计,并对此扩展模型展开基于模型转换的系统设计安全性特征的形式化分析与验证方法的研究;包括:构建了Sys ML活动图与MARTE中非功能性质建模语义相结合的元模型,以及验证工具UPPAAL的时间自动机元模型,并且给出了二者之间的语义映射规则;建立了从时间自动机模型描述到UPPAAL工具输入格式之间的语法转换方法;设计了一个基于AMMA平台的面向扩展Sys ML活动图的模型转换与验证框架;最后,给出了一个高铁控制系统设计模型的安全性验证的实例分析.     

智能合约函数的建模与验证研究

针对智能合约对安全性方面的相关性质的极高要求,有必要改进已有的建模算法,提出将智能合约函数的函数体语句建模为DTMC的算法,并对生成的DTMC进行验证.通过为状态迁移添加概率,实现了对随机现象的关注.通过对调用函数的分类处理,精细化了对函数调用函数情况的处理.通过添加标识符,实现了对智能合约所有控制语句的支持.对常被用...     

普适环境下智能模型的研究*

通过分析智能环境信息交互的特点和研究模型要实现的功能,定义一个动态智能空间四级模型,在涉及数据信息传递方面使用MPLS技术,实现了数据包在转发、传递过程中达到了低时延、低丢包率效果;在涉及用户信息的隐私保护方面,定义了一种隐私保护的模型,对用户在不同身份下的隐私信息提供保护。     

一种基于语义的安全协议形式化模型

在分析实际网络环境中安全协议的运行特点之后,提出了安全协议建模分析的两点基本假设.在此基础上,提出了一种基于语义的安全协议形式化模型,具体包括基于角色事件的协议静态描述模型和基于运行状态的协议动态执行模型,给出了模型的基本语法及形式语义,明确了模型推理过程中涉及到的一些关键性概念,并以简化的NSL协议为例进行了说明,为实现自动化验证打下了必要的基础.     

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.     

典型安全协议形式化分析工具比较

介绍了当前安全协议分析领域的典型形式化工具,阐述了其基本原理和在协议描述、归约、验证方面的研究现状,对它们的优缺点进行了综合比较,提出了如何在已有条件下开发协议分析工具的观点。     

电网企业移动智能终端的安全性分析

随着电力信息化进程的不断推进．移动应用也逐渐渗透电力运营的方方面面。但移动智能终端在给企业带来便利的同时,由于其便携性、系统开放性以及功能不断扩展等特点,也给企业带来巨大的安全威胁。在分析企业移动智能终端面临安全威胁的基础上,从硬件、操作系统、外围接口、应用软件和数据多个层面给出安全方案,保障电网移动业务安全稳定运行。     

安全协议的攻击分类及其安全性评估

对安全协议的安全性进行全面评估是十分重要的,但难度非常大．目前大量的研究工作主要集中于分析开放网络环境下安全协议的一些特定安全属性,例如,秘密性和认证性等．为了更全面地评估安全协议的安全防护能力,从攻击者的能力和攻击后果两个角度,提出一种新的安全协议攻击分类,并分析了不同攻击类型的特点与机理．在此基础上,探讨了安全协议的一种安全性评估框架,有助于更客观地评价安全协议的实际安全防护能力和设计新的协议．     

安全协议20年研究进展

总结了安全协议的20年研究进展情况，指出形式化方法在安全协议的设计与分析中的重要应用．对安全协议的若干热点研究方向进行了归纳和展望．     

认证协议两种形式化分析方法的比较

串空间模型和CSP方法是当前最著名的分析认证协议的形式化方法.通过一个具体的认证协议例子,比较两种方法的不同特点.     

Ad-hoc路由协议的串空间安全性扩展

根据Ad-hoc移动网络特点,深入分析了串空间模型的一致性条件,提出路由五段式模型,将中继者可信条件修改为任意中继者可信条件,使串空间适用于Ad-ho。安全路由协议分析。然后以一个攻击实例验证路由五段式模型的正确性和优越性。     

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

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