论文研究无线移动终端的SAV协议的形式化建模与模型检测.pdf

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