SIP协议的SPIN模型检测

计算机工程与应用 ›› 2014, Vol. 50 ›› Issue (13): 87-89.

SIP协议的SPIN模型检测

尤启房，杨晋吉

华南师范大学计算机学院，广州 510631

出版日期:2014-07-01 发布日期:2015-05-12

Model checking of SIP protocol via SPIN

YOU Qifang, YANG Jinji

School of Computer, South China Normal University, Guangzhou 510631, China

Online:2014-07-01 Published:2015-05-12

摘要/Abstract

摘要： 2010年Yoon等人提出一种基于椭圆曲线的三要素SIP认证密钥协商协议TAKASIP，但其存在一些攻击。对唐宏斌等人提出的该协议的改进方案使用SPIN进行了分析，发现仍然存在安全漏洞。针对这些缺陷，提出了一种有效的改进方案，采用在协议的消息中加入只有双方共享的秘密值的方法，克服了安全漏洞。新方案在不降低效率的情况下，提高了安全性。

关键词: TAKASIP协议, 椭圆曲线, SPIN工具, 模型检测

Abstract: In 2010, Yoon et al. proposed a three-factor authenticated key agreement scheme for SIP on Elliptic Curves named TAKASIP, but it exists some attacks. Using SPIN to analysis that the version given by Tang et al still exists an attack. Based on these flaws, an effective improvement for TAKASIP protocol is given, which adds a secret value only shared by both sides in the protocol and overcomes the security drawbacks. New scheme not only improves security but also maintains the high efficiency.

Key words: TAKASIP protocol, Elliptic curve, SPIN, model checking

尤启房，杨晋吉. SIP协议的SPIN模型检测[J]. 计算机工程与应用, 2014, 50(13): 87-89.

YOU Qifang, YANG Jinji. Model checking of SIP protocol via SPIN[J]. Computer Engineering and Applications, 2014, 50(13): 87-89.

[1]	陈虹，刘雨朦，肖成龙，郭鹏飞，肖振久. 基于BBS产生器和椭圆曲线的改进RC4算法[J]. 计算机工程与应用, 2020, 56(8): 87-95.
[2]	邓小鸿，朱年红，黄磊，王智强，王俊彬. 基于区块链的身份托管模型研究[J]. 计算机工程与应用, 2020, 56(4): 24-30.
[3]	李艳俊，汪书北，杨晓桐，曹贻森. 基于移动端的轻量级NFC安全认证方案[J]. 计算机工程与应用, 2020, 56(16): 84-89.
[4]	肖帅，王绪安，潘峰. 无模逆运算的椭圆曲线数字签名算法[J]. 计算机工程与应用, 2020, 56(11): 118-123.
[5]	张平，栗亚敏. 前向安全的椭圆曲线数字签名方案[J]. 计算机工程与应用, 2020, 56(1): 115-120.
[6]	许勇1，刘芬2. 异构传感网中避免中间人攻击的方案研究[J]. 计算机工程与应用, 2018, 54(22): 99-106.
[7]	李茜1，王峥1，马建芬1，李娜2. 轻量级移动支付协议公平性分析[J]. 计算机工程与应用, 2018, 54(19): 82-87.
[8]	李前利，江华. 命题μ-演算局部模型检测高效算法设计[J]. 计算机工程与应用, 2017, 53(9): 51-56.
[9]	张伟哲，高德智，李彦. 一个基于ECC的隐匿身份环签名方案[J]. 计算机工程与应用, 2017, 53(23): 88-90.
[10]	秦嫚蔓，王峥，王莉. 基于SPIN的远程证明协议的形式化分析及改进[J]. 计算机工程与应用, 2017, 53(1): 34-38.
[11]	李明. 新的适用于WSN网络的双方认证密钥协商协议[J]. 计算机工程与应用, 2016, 52(3): 100-102.
[12]	刘双根1，李欢1，李发根2. 一种抵抗Montgomery错误攻击的检错算法[J]. 计算机工程与应用, 2016, 52(24): 19-22.
[13]	吕江华1，刘志锋1，徐亚涛2，周从华1. 基于属性的访问控制策略的正确性验证[J]. 计算机工程与应用, 2016, 52(18): 98-103.
[14]	夏春蕊1，王瑞1，李晓娟1，关永1，张杰2，魏洪兴3. 动态环境下基于概率模型检测的路径规划方法[J]. 计算机工程与应用, 2016, 52(12): 5-11.
[15]	黄延凯，周宇，魏欧. 新型属性图文法反应式规约验证方法[J]. 计算机工程与应用, 2016, 52(12): 15-18.