中文摘要：

随着移动应用广泛普及，移动通信的安全要求就愈来愈高，而移动设备计算能力相对较低，如何降低移动端的计算量是移动通信的认证密钥协商协议需要解决的问题．为了降低通信中移动端的计算量，很多用于移动设备的身份认证协议采用哈希函数代替签名机制进行身份认证，而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.