无线移动终端的SAV协议的形式化建模与模型检测

• 作者: 杨翰文 谢光颖 龙士工
• 来源期刊: 计算机应用研究
• 关键词: 服务器辅助验证协议 模型检测 NuSMV工具 有限状态机 计算树逻辑
• 年，卷（期）: 2014,（6）
• 页码范围: 1877-1879,1882
• 页数: 4页
• 分类号: TP309
• 语种: 中文
• DOI: 10.3969/j.issn.1001-3695.2014.06.065

摘要

公钥数字签名方案中验证方是低运算能力的移动智能设备时,验证方在验证过程中需要借助于服务器来辅助验证.SAV(server-aided verification)协议是一个对无线移动终端实现辅助计算和签名验证的协议,利用有限状态机对该协议中签名方、验证方以及服务器进行形式化建模,并使用NuSMV工具对SAV协议模型检测,目的是验证该协议的签名方案有效性、防欺骗性和不可否认性.实验结果表明该协议存在服务器和签名方联合欺骗和否认的缺陷,最终分析其原因和提出针对性的改进方案.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	龙士工	贵州大学计算机科学与信息学院	39	110	5.0	9.0
2	谢光颖	贵州大学计算机科学与信息学院	2	1	1.0	1.0
3	杨翰文	贵州大学计算机科学与信息学院	2	1	1.0	1.0