新的移动支付协议及其形式化分析
来源：计算机应用与软件杂志2025年第11期北京时间：
作者：石庆霞, 汪学明
摘要：针对移动支付协议的认证子协议中未对商家身份认证容易遭到恶意商家的匿名攻击和协议未考虑时限性以至于无法确保交易进行的正确性的问题，提出一种新的移动支付协议。新协议通过对商家身份进行认证和引入了时间戳服务器T，实现了用户和商家的双向认证和时限可追究性。通过SVO逻辑和时限逻辑对新移动支付协议进行形式化分析，新的移动支付协议满足双向认证性和时限可追究性。
关键词：移动支付协议, 双向认证, 时限性, SVO逻辑, 时限逻辑, 形式化分析
