摘要
随着移动应用广泛普及,移动通信的安全要求就愈来愈高,而移动设备计算能力相对较低,如何降低移动端的计算量是移动通信的认证密钥协商协议需要解决的问题.为了降低通信中移动端的计算量,很多用于移动设备的身份认证协议采用哈希函数代替签名机制进行身份认证,而SVO逻辑缺乏对哈希函数用于身份认证的形式化描述.因此,扩展了SVO逻辑分析哈希函数的逻辑语法,增加了相应的推理公理,证明了推理公理的安全性.然后,讨论了SVO逻辑方法的分析目标,举例证明了其实体认证目标存在的漏洞,提出新的认证目标,同时分析了新目标的安全性.实验证明,对SVO逻辑方法的扩展与改进是实用和有效的,此工作对其他的安全协议形式化分析方法也具有借鉴意义.
Mobile applications are popular, hence secure mobile communication is a necessity. Unfortunately, the computational ability of mobile terminals is relatively low, so it is urgent to reduce the computational complexity of authentication and key agreement protocols in mobile communication. To reduce computational demands, many authentication protocols used in mobile terminals adopt hash functions, instead of signatures, for authentication. Nevertheless, SVO logic lacks a formalized description for authentication of hash functions. This paper proposes extensions to the syntax of SVO logic for the analysis of hash functions, adding corresponding axioms of reasoning （algorithms） and proving its security. Goals of SVO logic are then discussed, showing this method satisfies the default goals in ＂Entity authentication＂. Finally, a new authentication goal is proposed, and security of the new goal is analyzed. Practice has proved that expansion and improvement of SVO logic are practical and effective, compared to other security protocols.
出处
《哈尔滨工程大学学报》
EI
CAS
CSCD
北大核心
2007年第5期542-547,共6页
Journal of Harbin Engineering University
基金
国家自然科学基金资助项目(30400446)
2CNGI示范工程2005年研究开发
产业化及应用试验基金资助项目(发改办高技[2004]2482号)
关键词
哈希函数
SVO逻辑
实体认证
密钥确认
形式化分析
hash function
SVO logic
entity authentication
key confirmation
tormalized analysis
