对SVO逻辑方法的改进

作     者：吴开贵 陈明 WU Kai-Gui;CHEN Ming

作者机构：重庆大学计算机学院重庆400044 

出 版 物：《哈尔滨工程大学学报》 (Journal of Harbin Engineering University)

年 卷 期：2007年第28卷第5期

页      面：542-547页

核心收录：

学科分类：0817[工学-化学工程与技术] 0839[工学-网络空间安全] 08[工学] 0807[工学-动力工程及工程热物理] 0827[工学-核科学与技术] 0802[工学-机械工程] 0703[理学-化学] 0825[工学-航空宇航科学与技术] 0811[工学-控制科学与工程] 0801[工学-力学（可授工学、理学学位）] 

基　　金：国家自然科学基金资助项目(30400446) 2CNGI示范工程2005年研究开发 产业化及应用试验基金资助项目(发改办高技2482号) 

主　　题：哈希函数 SVO逻辑 实体认证 密钥确认 形式化分析 

摘      要：随着移动应用广泛普及,移动通信的安全要求就愈来愈高,而移动设备计算能力相对较低,如何降低移动端的计算量是移动通信的认证密钥协商协议需要解决的问题.为了降低通信中移动端的计算量,很多用于移动设备的身份认证协议采用哈希函数代替签名机制进行身份认证,而SVO逻辑缺乏对哈希函数用于身份认证的形式化描述.因此,扩展了SVO逻辑分析哈希函数的逻辑语法,增加了相应的推理公理,证明了推理公理的安全性.然后,讨论了SVO逻辑方法的分析目标,举例证明了其实体认证目标存在的漏洞,提出新的认证目标,同时分析了新目标的安全性.实验证明,对SVO逻辑方法的扩展与改进是实用和有效的,此工作对其他的安全协议形式化分析方法也具有借鉴意义.