| 一种移动支付协议的模型检验分析 |
| |
| 引用本文： | 刘霞,古天龙,郭云川. 一种移动支付协议的模型检验分析[J]. 计算机工程与应用, 2006, 42(33): 46-49,52 |
| |
| 作者姓名： | 刘霞 古天龙 郭云川 |
| |
| 作者单位： | 桂林电子工业学院,计算机系,广西,桂林,541004;桂林电子工业学院,计算机系,广西,桂林,541004;桂林电子工业学院,计算机系,广西,桂林,541004 |
| |
| 摘 要： | 给出了移动支付协议的一种有限状态机建模方法,该方法在传统支付协议的基础上充分考察了移动环境中移动装置和无线网络的特点,所建立的模型具有全面、准确、直观、简洁的特点。以一个典型的移动支付协议KSL为例,对该协议进行有限状态机建模,并通过模型检验工具对其公平性进行了分析验证,指出了其缺陷并进行了改进,从而表明了方法的有效性。该方法具有一定的通用性,以其为基础,可对其他类型的移动电子商务协议进行模型检验分析。
|
| 关 键 词： | 移动支付协议 模型检验 公平性 |
| 文章编号： | 1002-8331（2006）33-0046-04 |
| 收稿时间： | 2006-02-01 |
| 修稿时间： | 2006-02-01 |
Model Checking Analysis of Mobile Payment Protocols |
| |
| LIU Xia,GU Tian-long,GUO Yun-chuan. Model Checking Analysis of Mobile Payment Protocols[J]. Computer Engineering and Applications, 2006, 42(33): 46-49,52 |
| |
| Authors: | LIU Xia GU Tian-long GUO Yun-chuan |
| |
| Affiliation: | Department of Computer,Guilin University of Electronic Technology,Guilin,Guangxi 541004,China |
| |
| Abstract: | 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. |
| |
| Keywords: | mobile payment protocols model checking fairness |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
