基于RGPS服务本体交互建模分析与验证

在动态、异构和自治的互联网服务环境中,对WEB服务组合的形式化分析与验证是保证按需服务应用的有效途径,寻找有效的形式化分析方法和工具是热点领域.针对现有研究主要是集中于服务组合流程和静态结构方面,而在动态反映用户需求的服务组合及支持服务的动态耦合存在不足.本文从服务本体的语义层面,通过对OWL-S进行RGPS属性扩充,研究SOA架构模型映射到Pi演算的进程模型,对动态耦合的按需服务组合进行形式化分析并用Pi演算验证工具MWB进行验证.实验结果表明方法的可行性,为按需动态服务组合的有效性分析提供了一种验证方法.     

并发系统中谓词行为图的行为时序逻辑表达

行为时序逻辑(TLA)组合时序逻辑与行为逻辑, 可以对并发系统进行描述与验证, 它引入动作和行为的概念, 使得系统和属性可用它的规约公式表示, 但存在用TLA描述复杂系统时TLA公式复杂且难以理解的不足。类似于状态转移图, 对于并发转移可以用谓词行为图进行图形化表示, 谓词行为图与行为时序逻辑规约具有相同的表达能力。介绍行为时序逻辑的语法、语义及简单推理规则, 用一个简单的实例说明使用谓词行为图去描述并发转移系统的有效性, 并用系统规约的TLA公式对谓词行为图表达能力进行证明, 表明两者具有等价性, 为描述和分析并发转换系统提供了一种可行的方法。     

一种目标感知的可配置业务流程分析方法

可配置业务流程模型能够使得在不同的组织之间以可控的方式共享公共流程成为可能,这种模型旨在通过配置满足特定组织的需求,派生出个性化的流程.流程配置由于其配置决策之间的各种依赖关系而变成异常困难,因此,对其进行形式化建模和验证是一个非常重要的问题.由于目标模型能够良好的表达用户需求意图的特点,本文提出一个基于目标感知的可配置业务流程分析方法,这种方法是通过将目标关联到WF-net(即GWF-net),将用户需求意图与业务流程模型进行整合;然后通过增加配置操作将用GWF-net表达的业务流程模型转换成可配置业务流程模型;最后,分析这种可配置业务流程的逻辑结构的正确性并提出用户需求与可配置业务流程配置过程中的一致性定理,为分析与验证在目标约束下可配置业务流程提供一种行为有效的方法.     

基于RO模型的公钥加密方案安全性分析与证明

信息安全是信息社会存在的根基,而密码学是信息安全技术的核心部分,因此,对密码方案或协议的设计与应用的安全性成为人们最为关注的问题。本文首先介绍随机预言模型(RO)及相关的归约论断和敌手模型定义,并运用这种模型对公钥加密方案进行了安全性分析,同时给出了证明,结果达到预期的安全性目标。     

一种基于RGPS着色的C-net模型及其应用

可配置业务流程模型描述面向领域的相似流程模型家簇,这种模型能够通过配置操作获取满足特定用户需求的个性化流程模型.提出一个在角色和目标约束下以流程为中心的可配置业务流程模型,首先对因果网模型(C-net)进行扩展,将该模型中的活动元素增加角色和目标两个约束关系,从而利用RGPS需求元模型框架中对角色(R)、目标(G)、流程(P)、服务(S)之间的约束规则和关联关系去约束业务流程活动之间的执行序列,使得模型有效反映了业务流程活动中的实际行为;然后将活动的输入绑定和输出绑定端口设置配置操作标记,通过对端口配置标记的操作形成个性化流程;最后,给出了模型的形式化定义并分析模型在业务流程配置中的应用,使得能够指导业务流程的配置等管理操作.     

一种可用于光学密码的安全增强工作模式

 为满足云计算对高安全、高效率密码方案的需求,该文提出一种安全增强密码工作模式——密码反馈“一组一密”(Cipher FeedBack one Block one Key, CFB-BK)模式,并基于数学密码和光学密码组合实现：光学密码对数据分组进行“一组一密”加解密,数学密码利用光学密码密文生成供光学密码下一组数据加解密使用的密钥。安全性分析表明,攻击者在密码学技术范围内,只能采用穷举密钥攻击方式,攻击复杂度高;效率分析表明,比基于数学密码实现的模式效率更高。     

基于TLA的NS安全协议分析及检测

行为时序逻辑是一种组合了时序逻辑与行为逻辑来对并发系统进行描述与验证的逻辑,在描述并发转移系统中,行为时序逻辑通过引入行动和行为的概念,使得系统和属性可用同一种行为时序逻辑来表示。本文首先介绍行为时序逻辑的语法、语义及简单推理规则;然后以典型的NS公开密钥协议为例,对其进行形式化分析,建立了入侵者参加的简化模型。通过对模型进行FSM建模,转化为TLA+描述的规约系统,然后对其进行TLC检测,发现其存在中间人的重放攻击。     

光学密码在车联网中的应用

车联网将是物联网应用研究热点。车联网需要安全性和高效性,如果采用传统加密技术,安全性和高效性存在矛盾。光学密码是一种并行密码算法,可以有效解决这一问题,但其自身的实现存在一些困难。论文将光学密码用于车联网系统,是一种很好的理论探讨研究。     

基于IP欺骗的SYN泛洪攻击

网络层的传输控制协议(TCP)向用户提供面向连接、高可靠性端到端服务,但TCP协议缺乏认证等相关功能,使得在网络层的通信存在很大的安全隐患,因此,需要对此攻击进行分析,找出这种攻击的关键点,模拟这种复合攻击,然后采取相应的预防措施.介绍TCP三次握手协议工作机制,并作了简单的形式化分析,同时分析了基于IP欺骗的泛洪攻击原理,在此基础上实现这种网络攻击技术并作相应的防范分析,从而为网络安全分析提供行之有效的方法.