互联网 qkzz.net
全刊杂志网:首页 > 女性 > 文章正文
刊社推荐

调和安全协议两种分析方法的理论研究


□ 朱玉娜 王亚弟 韩继红 范钰丹

  摘要:安全协议形式化分析方法分为两种,即符号方法和计算方法。比较两种方法,它们各有优缺点。目前,将两者进行组合优化,建立统一的调和方法框架对安全协议进行分析是研究的热点和难点。针对该问题,对目前国际上流行的相关方法进行了分类总结,并对涉及到的技术手段进行了全面分析。
  关键词:安全协议; 符号方法; 计算方法; 密码学可靠性
  中图分类号:TP309文献标志码:A
  文章编号:1001-3695(2008)03-0930-04
  
  安全协议形式化分析研究领域存在两种完全不同的方法:a)符号方法,大多基于DolevYao模型,采用模型检测或定理证明来分析安全协议;b)计算方法,基于计算复杂性理论,安全证明采用归约分析。这两种方法各有优缺点:符号方法可有效实现自动化,但会遗漏从底层密码算法或密码算法与协议的交互中产生的一些安全问题,不能真正建立起密码学的可靠性;计算方法是密码学可靠的,但多采用手工证明,自动化程度较低。因此,结合两种方法的优点,将两者组合到一个框架中对安全协议进行形式化分析就成为当前备受关注的研究内容。
  目前对于符号方法与计算方法的调和方法研究主要集中在两个方面:一方面侧重于符号方法的调和方法研究;另一方面侧重于计算方法的调和方法研究。
  
  1侧重符号方法的调和方法研究
  
  侧重符号方法的调和方法是从符号方法的角度来减少分析安全协议时所作的基本假设(如假设密码系统是完美的),在较低的抽象层次上对安全协议进行形式化分析,改善形式化证明与协议具体执行过程的联系,从而建立起形式化方法的密码学可靠性。目前,研究方法主要有逻辑、模拟、LMMS以及密码学扩充四种方法。前三种是研究的主流方法,其主要思想是用理想功能和不可区分来描述证明协议的组合安全性质,即实际协议的安全性通过与理想协议或理想功能的对比来描述。
  1.1逻辑方法
  在逻辑方法框架中定义了逻辑集合和计算集合,逻辑描述可以在计算集合中表示。如果在逻辑集合中可以证明出某安全命题,则在计算集合中此安全命题的计算解释也是有效的。逻辑方法的优点在于逻辑上的简洁性;其缺点在于逻辑上的抽象性过高,这种抽象往往会掩盖(或丢失)协议执行的状态信息,难以完全反映协议运行的全貌。这方面的代表性方法是AbadiRogaway方法。
  1.1.1AbadiRogaway方法
  M. Abadi等人[1]于2000年首次综合符号方法和计算方法,提出了AbadiRogaway方法。此方法证明了如果两个表达式在逻辑公式下等价,则在计算复杂性下它们所生成的概率分布也是计算不可分的。
  它首先在逻辑模型中定义一个表达式类和表达式等价关系。表达式代表数据,由原子消息和密钥通过对偶、对称加密构建。接着为形式化的消息定义了模式pattern(pattern由原子消息、密钥、对偶、对称加密以及不可解密组成。形式化消息的pattern比消息本身的结构简单。直观上,pattern是表达式集合的扩展,它增加了攻击者不能解密的消息表达式类型)。表达式等价当且仅当它们能产生相同的pattern。此等价关系抓住了对攻击者而言数据看起来一样这一特征。逻辑模型中的这些定义十分简单,不需要概率和计算复杂性的任何概念。 ......
很抱歉,暂无全文,若需要阅读全文或喜欢本刊物请联系《计算机应用研究》杂志社购买。
欢迎作者提供全文,请点击编辑
分享:
 

了解更多资讯,请关注“木兰百花园”
分享:
 
精彩图文


关键字
支持中国杂志产业发展,请购买、订阅纸质杂志,欢迎杂志社提供过刊、样刊及电子版。
关于我们 | 网站声明 | 刊社管理 | 网站地图 | 联系方式 | 中图分类法 | RSS 2.0订阅 | IP查询
全刊杂志赏析网 2017