一种移动支付协议的模型检验分析  

Model Checking Analysis of Mobile Payment Protocols

作　　者：刘霞[1] 古天龙[1] 郭云川[1] 

机构地区：[1]桂林电子工业学院计算机系,广西桂林541004

出　　处：《计算机工程与应用》2006年第33期46-49,52,共5页Computer Engineering and Applications

摘　　要：给出了移动支付协议的一种有限状态机建模方法,该方法在传统支付协议的基础上充分考察了移动环境中移动装置和无线网络的特点,所建立的模型具有全面、准确、直观、简洁的特点。以一个典型的移动支付协议KSL为例,对该协议进行有限状态机建模,并通过模型检验工具对其公平性进行了分析验证,指出了其缺陷并进行了改进,从而表明了方法的有效性。该方法具有一定的通用性,以其为基础,可对其他类型的移动电子商务协议进行模型检验分析。A modeling approach of FSM （Finite State Machine） is proposed,where the features of mobile device and wireless network in mobile environments are considered.As an example,fairness of a typical mobile payment protocol KSL is analyzed using model checking.As a result,some defects of the protocol are pointed out and an improvement is proposed,which shows that our approach is effective.In addition,our approach is generic and it can be used to analyze other kinds of mobile electronic commerce protocols.

关 键 词：移动支付协议 模型检验 公平性 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]