计算可靠的密码协议形式化分析综述

密码协议的描述和分析有两类截然不同的方法:一类以形式化方法为主要手段,另一类以计算复杂性理论为基础.Abadi和Rogaway首次试图将这两类不同的方法关联起来,证明一个协议在形式化模型下具有某种安全属性,那么在计算模型下也保持相应的安全属性.在这一工作的带动下,形式化方法的计算可靠性研究越来越受到关注,成为密码协议分析研究的一个重要内容.围绕这一热点问题,人们做了大量的工作.该文首先对两类分析方法做概要介绍;其次对形式化分析的计算可靠性研究成果进行分类和总结,并对各种方法的主要思想进行了介绍;最后对该领域未来的研究方向进行了展望.     

一种开放的综合安全模型

为了在信息系统的安全模型中反映综合化的安全需求,以基于角色的访问控制模型为基础,通过对安全级等方面的扩展,提出一种开放综合安全模型（OSSM）.根据OSSM的开放性,通过扩充其基本元素,完成了对一种保密性和完整性的综合模型以及Clark-Wilson模型的实现,拓宽了安全模型的适用范围.     

一种时间相关安全协议的自动验证工具

设计并实现了一个时间相关安全协议的自动验证工具。工具以一种时间相关安全协议逻辑TCPL为基础,以XML语言为描述方式,采用构造分层逻辑树的方法,完成了对安全协议目标的自动验证。实现结果表明,该工具简化了安全协议的证明过程,提高了效率,具有较好的实用性。     

对一种公平非否认协议的新改进

Zhou-Gollmann协议是一种公平非否认协议,近年来得到广泛讨论.Kim发现该协议在时限公平性方面存在缺陷,针对该缺陷提出一种改进的协议,但其改进方法高度依赖于网络时钟的同步.通过详细分析,发现在缺乏时钟同步时Kim的改进协议也可导致不公平.针对此问题,提出一种新的改进方案.新的改进消除了协议对时钟同步的依赖性,保持了协议的公平非否认性,且不会降低协议的效率.     

时间相关密码协议逻辑及其形式化语义

在密码协议中,主体的认知与信仰状态是随时间推移而不断变化的.为了在协议分析中体现这种动态性,提出一种时间相关密码协议逻辑.该逻辑基于谓词模态逻辑,通过在谓词及模态词中引入时间参数以体现时间因素,使得逻辑可表达各个主体在协议不同时间点的行为、知识及信仰.给出该逻辑的形式化语义,在避免逻辑语言二义性的同时保证了逻辑的可靠性.该语义基于Kripke结构,将可能世界建立在主体局部世界与时间局部世界的基础上,使得任一可能世界能够反映协议的一个可能的全过程.该逻辑为密码协议,特别是时间相关密码协议提供了灵活的分析方法,增强了基于逻辑方法的协议分析能力.     

可视化的安全策略形式化描述与验证系统

通过分析安全策略中可能出现的问题,对安全策略的一致性与完备性进行形式化定义。通过构造安全策略的状态模型,提出策略的一致性与完备性验证算法。基于可扩展访问控制标记语言,设计并实现一种安全策略的形式化描述与验证系统。该系统将形式化的验证过程自动化,以可视化的形式为普通用户提供一种高效的策略验证工具。     

Chinese-Wall模型在开放综合安全模型中的实现

Chinese Wall模型体现了随系统运行而不断改变的动态安全策略,但使用范围有限. 为了保持安全模型在适应不同领域的同时能够体现动态安全策略,基于一种开放的综合安全模型(OSSM),提出Chinese Wall模型的实现方法.该方法通过构造动态累加角色,记录必要的访问历史,然后结合历史访问及安全策略对当前访问请求作出决策,以体现策略的动态性.实现结果表明,该方法在保持模型综合性的同时,提高了其灵活性.     

改进Athena算法的多协议攻击自动化验证方法

多协议环境下协议安全性问题是安全协议形式化分析验证领域的一个公开问题。针对此问题,在分析Athena算法的基础上提出了一种多协议攻击自动化验证方法。该方法扩展了Athena状态表示方法和后继状态生成算法,使得攻击者具备截取其它协议交互消息和计算生成当前协议消息的能力,能够以自动化的方式验证协议是否存在多协议攻击。实验结果表明,提出的方法能够实现多协议攻击的自动化验证。