基于进程演算和知识推理的安全协议形式化分析

安全协议的形式化分析是当前安全协议研究的热点,如何扩充现在已经成熟的理论和方法去研究更多的安全性质,使同一系统中各种安全性质在统一的框架下进行分析和验证是一个亟待解决的问题.进程演算是一强有力的并发系统建模工具,而结合知识推理可以弥补进程演算固有的缺乏数据结构支持的特点,以此提出了一个安全协议形式化分析的一般模型.基于此模型,形式化地定义了一些安全性质,给出了一个实例研究,并指出了进一步完善此模型的研究方向.

移动进程演算中的开互模拟

该文就移动进程演算中的弱开同余关系进行研究 .文中考虑了一种简单的非确定性移动进程演算模型 ,证明了 Milner的三条 tau规则在有等名测试算子时不足以将强开同余关系的完全公理化系统提升到弱开同余关系的完全公理化系统 .文中提出了第四条 tau规则 ,处理了在前缀操作下的等名测试算子 ,并证明了强开同余关系的完全公理化系统加上四条 tau规则可得到弱开同余关系的完全公理化系统 .该文的结论否定了关于 Milner的三条

一个移动进程演算的互模拟同余定义框架

并发计算模型是理论计算机科学研究的重要领域之一。以π演算为代表的移动进程演算是目前并发理论的研究热点。互模拟等价定义是移动进程演算研究中的核心概念和问题,而传名机制使得移动进程演算中的互模拟同余关系更加复杂和有趣。本文在分析了常见的互模拟同余定义的基础上,通过抽取定义的核心要素,提出了一个三维的互模拟同余定义模型,从而将一般文献中常见的互模拟定义纳入到一个统一的框架中来,加深了我们对移动进程演算中互模拟概念的理解;同时本文利用这个模型,系统分析了各种互模拟之间的关系。模型的优点在于它的普适性和开放性。

基于进程演算的公钥密码体制安全性自动化证明系统

可证安全是一种通过严格证明确保密码体制安全性的形式化方法,但由于其证明结论严重依赖于证明者个人的经验和技巧,这一方法本身的可靠性受到了质疑。文章设计并实现了一套公钥密码体制安全性自动化证明系统,使用一种概率多项式时间进程演算描述可证安全模型,借助进程间的互模拟等价关系和进程约减实现基于游戏的可证安全自动化证明。系统在C语言环境下实现,已完成ElGamal加密体制和FDH签名体制在内的一系列密码体制的安全性证明测试。

有界Petri网的进程演算表达

为了进一步探讨Petri网与进程演算的关系,给出了一种使用进程演算模型(CCS)表示有界Petri网的方法.对于任意的有界Place/Transition网,可以用该方法构建一个与之相对应的有限进程.并且证明了所得进程与原网之间满足操作一致性和观察一致性.同时,证明了该方法在网的标号互模拟上满足完全抽象性.

区间值进程演算的可加模型

进程演算是研究并行计算和分布式计算的一个重要语义模型．引入区间值进程演算的可加模型(简称AICCS),以解决在并发通讯系统中产生的不确定性．在该模型中,前缀进程、并行进程以及和进程都赋以区间值．作者给出了AICCS的语法及可加的操作语义,引入了进程的量化这一概念,在此基础上引入强互模拟和μ-强互模拟的概念,并且讨论了其相关性质．

Ambient演算的框架设计

给出Ambient演算的一种内部表示,称为Ambient框架,并给出了Ambient框架的构造方法和具体转换函数,以及基于Ambient框架的执行操作语义.该框架为异步、分布和移动代码提供了语言支持.

消除有限容量演算中的强干扰

为了消除有限容量演算中的强干扰和控制资源的移动,改进了该演算的某些原语,提出了一种新的演算——安全有限容量演算.在新演算中,调整了2个能力,增加了3个能力(相当于动作)和2个余能力(余动作),并改进相应的归约语义,给出了安全有限容量演算的类型系统.该类型系统控制灰箱的移动性和线程数,并保证在计算过程中灰箱所拥有的资源数被静态地保持在其资源数范围内.

基于进程代数的构件语义标注技术研究

针对组合构件的语义标注问题,提出基于进程代数的自动标注方法,以减小构件库开发人员手工标注大粒度组合构件语义的工作量。采用本体描述构件的语义,对于不同结构的组合行为,通过进程演算抽取交互行为的执行序列,给出组合构件语义的抽取、合成方法及相应的语义标注算法。将该技术集成到JTangComponent平台上进行实验,结果标明其提高了语义标注的自动化程度,可以为复用构件提供语义保障。

带Mismatch算子的高阶π演算

主要研究带mismatch的高阶进程演算的公理化问题.首先,建立存在mismatch时高阶进程的开弱高阶互模拟理论,证明了等价关系、同余性等重要性质;其次,沿用线性的方法,构建得到带mismatch的有限进程上的公理系统;最后,基于对开弱高阶互模拟的刻画,证明了该公理系统的完备性定理.该工作为带mismatch的高阶进程上互模拟判定的有效算法的设计与实现,进而为相关的应用建模工作提供了理论借鉴.

非对称带不等算子的χ~≠-演算(英文)

文章系统研究非对称带不等算子χ≠-演算进程上的互模拟.通过构造互模拟格,从全部L-互模拟关系中导出12个互异的L-互模拟关系,研究了这些关系所对应的同余关系和迟早开同余关系.提出3个更新律,并修改了3个τ律.最后,给出了14个同余关系的可靠完备系统.

用进程代数描述面向电子商务的Agent模型

演算作为一种刻划通信系统的进程演算在刻划Agent间的交互时具有得天独厚的优势。该文用多价演算来描述面向电子商务的Agent间的通信流程 ,力图通过这种形式化的方法 ,清楚描述软件Agent在电子商务的交易过程中的重要作用 ,并对软件agent在电子商务中的实现有所帮助。

量子进程

由量子力学原理,酉变换和测量算子可以完成量子计算中的所有操作,但仅用酉变换和测量算子的序列并不能清楚地描述量子世界的并发与通信,因此本文提出了量子进程的概念,讨论量子进程通信的几种可能方式,并基于CCS建立了两个量子进程的一种互模拟关系,用以刻画传送量子进程的并发与通信。

进程的归约

给出了进程归约语义的一般方法．并用例子说明归约语义和转换语义的对应关系．

构件组装及其形式化推导研究

基于构件的软件工程(component based software engineering,简称CBSE)能够有效地提高软件开发的质量和效率.构件组装和组装推导(compositional reasoning)是CBSE的关键技术.基于软件构件的特点,借鉴进程代数中进程构造的方法,提出6种构件组装机制,能够灵活、简便地集成软件构件,并主张在构件组装的同时进行接口组装,通过生成功能更强、抽象级别更高的复合接口,提高构件组装的抽象级别和粒度.同时,基于Wright的形式化规约软件体系结构的研究,给出了复合构件和复合接口的组装推导算法,为系统行为的形式化分析、验证和仿真奠定了基础.

基于可达关系的安全协议保密性分析

借助形式化的方法或工具分析安全协议是非常必要而且行之有效的.进程演算具有强大的描述能力和严格的语义,能够精确刻画安全协议中各个参与者之间的交互行为.作者以进程演算为基础,嵌入消息推理系统以弥补进程演算固有的缺乏数据结构支持的特点,尝试地提出了一个基于可达关系的安全协议保密性分析模型.基于此模型,形式化地描述了安全协议的保密性,证明了一定限制条件下的可判定性.并且以TMN协议为例,给出了该模型的实例研究.

Web服务降级替换的一致性问题及量化研究

在开放的网络环境下,软件系统的可信性受到了更大的挑战,软件系统的降级替换是提高其可信性的方法之一。基于进程代数研究了Web服务的降级替换问题。在原有进程代数的基础上,添加了超时处理算子和延时处理算子,给出了Web服务降级替换一致性条件,从而保证了合成Web服务中降级替换的正确性。进一步地,从量化角度对Web服务的降级替换进行了研究。

一种安全协议的组合分析模型研究

在当前安全协议形式化分析的研究中,亟待解决的关键问题是如何形式化描述更多的安全属性,如何将这些属性在统一的框架下进行形式化分析和验证.本文提出了一种统一的安全属性形式化描述方法,在此基础上,利用知识推理来弥补进程演算缺乏数据结构的固有缺陷,从而提出了一种安全协议形式化分析的一般组合模型.通过实例分析验证了模型的有效性,并指出了该模型的研究方向.

可证明安全性自动化证明方法研究

可证明安全性是密码协议安全性评估的重要依据,但手写安全性证明容易出错且正确性难以判定。该文论述了基于游戏(Game based)转换的安全性证明及其自动化实现方法,重点论述了基于进程演算的自动化证明方法,并以该方法研究OAEP+的自动化安全性证明,首次给出了其初始游戏和相关的观察等价式。

基于逻辑编程的EKE协议分析

基于逻辑编程规则及Spi演算提出了一种验证密码协议安全性的新方法,利用该方法可以对密码协议的安全性质以程序化的方式进行验证。通过对EKE协议进行的分析,不但证明了协议已知的漏洞,而且发现了针对EKE协议的一个新的攻击——并行会话攻击。很好地验证了该新方法对密码协议的分析能力。