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

Formal modeling and model checking of SAV protocol in wireless mobile terminal

作　　者：谢光颖 龙士工[1] 杨翰文[1] 

机构地区：[1]贵州大学计算机科学与信息学院,贵阳550025

出　　处：《计算机应用研究》2014年第6期1877-1879,1882,共4页Application Research of Computers

基　　金：国家自然科学基金资助项目(61163001)

摘　　要：公钥数字签名方案中验证方是低运算能力的移动智能设备时,验证方在验证过程中需要借助于服务器来辅助验证。SAV(server-aided verification)协议是一个对无线移动终端实现辅助计算和签名验证的协议,利用有限状态机对该协议中签名方、验证方以及服务器进行形式化建模,并使用NuSMV工具对SAV协议模型检测,目的是验证该协议的签名方案有效性、防欺骗性和不可否认性。实验结果表明该协议存在服务器和签名方联合欺骗和否认的缺陷,最终分析其原因和提出针对性的改进方案。For the current public key digital signature scheme,when the verifier is the mobile smart devices which is too weak to calculate,verifier in the verification process need the aid of a powerful server to assist in the verification process.SAV （serveraided verification） protocol is a security protocol of calculation-aid and signature verification with server for wireless mobile terminals.This paper modeled the prover,verifier and server of SAV protocol with the finite state machine and verified possible deception and denial behavior using NuSMV tools.The result showed that the protocol defects were found,then it analyzed the reasons and proposed viable solutions.

关 键 词：服务器辅助验证协议 模型检测 NuSMV工具 有限状态机 计算树逻辑 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]