基于时间自动机的移动支付协议的形式化验证及实例

《基于时间自动机的移动支付协议的形式化验证及实例》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、学校代码10459学号或申请号201312172065密级硕士学位论文基于时间自动机的移动支付协议的形式化验证及实例作者姓名：吴格格导师姓名：庄雷教授王瑞民副教授学科门类：工学专业名称：软件工程培养院系：信息工程学院完成时间：2016年5月AthesissubmittedtoZhengzhouUniversityforthedegreeofMasterFormalverificationandinstanceofmobilepaymentprotocolbasedontimedautomataByGegeWuSupervisor：Pro

2、f.LeiZhuangandAssociateProf.RuiminWangSoftwareEngineeringSchoolofInformationEngineeringMay,2016学位论文原创性声明本人郑重声明：所呈交的学位论文，是本人在导师的指导下立进行研，独究所取得的成果。除文中已经注明引用的内容外，本论文不包含巧何其他个人或集体已经发表或撰写过的科研成果。对本文的研巧作出重要贡献的个人和集体，均己在文中明确方式标明＝本声明的法律责任由本人承担。学位论文作者；嫌焉曰期：站／年ｉ月曰名诚学位论文

3、使巧授权声明．本人在导师指导下完成的论文及相关的职务作品．，知识产）Ｉ权归属郑；Ｉ大学。根据郑州大学有关保留、使用学位论文的规定，同意学校保留或向国家有关部口或机构送交论文的复印件和电子版，允许论支被查阅和借阅；本人援权郑州大学可Ｗ将本学位论文的全部或部分编入有关数据库进行检索，可Ｗ采用影印、缩印或者其他复制手段保存论文和汇编本学位论文。本人离校后发表、使用学位论文或与该学位论文直接相关的学术论文或成果时一，第署名单位仍然为邦州大学■Ｃ保密论文在解密后应遵守此规定。学位论文作者；銀提曰期：么４年

4、月曰Ｉ７０摘要摘要随着移动支付的广泛应用，移动支付协议作为安全性的重要保障，已经成为了学术界的研究热点之一。为了保证移动支付协议的安全性和正确性，需要对移动支付协议进行形式化分析、建模和验证。但是移动支付协议是在移动环境中执行的，而且用户使用的移动设备在电量、计算能力和存储空间方面均受到限制，这些约束都给移动支付协议的形式化分析、建模和验证提出了新的挑战。因此，研究移动支付协议的形式化分析、建模和验证具有重大的意义。根据移动通信的不同场景，JesúsTéllezIsaac等人提出了使用对称加密技术以支付网关为中心的安全支付协议PCM

5、S(SecurePaymentCentricModelusingSymmetriccryptographyprotocol)，并在真实环境下对PCMS协议的执行时间和内存空间进行了分析和评估。结果表明，在服务器中心模型下，PCMS协议计算量少。但是未对PCMS协议的安全性质进行形式化分析和验证，因此在实际生活中并没有得到广泛应用。本文基于时间自动机对移动支付协议进行了建模。分别对系统主体、通信环境和主体操作进行了描述，并采用时间自动机对移动支付协议进行建模和分析。在使用时间自动机对移动支付协议建模的基础上，本文选取使用对称加密技术以支付

6、网关为中心的安全支付协议PCMS为研究对象，使用模型检测工具UPPAAL对PCMS协议进行了分析和验证。结果表明，PCMS支付协议满足无死锁、时效性、有效性和钱原子性。关键词：移动支付协议模型检测时间自动机UPPAAL支付协议验证IAbstractAbstractWiththewideapplicationofmobilepayment,mobilepaymentprotocolisanimportantguaranteeofitssecurity,hasbecomearesearchfocusintheacademia.Toensur

7、ethesafetyandcorrectnessofmobilepaymentprotocol,weneedtoformalmodeling,analysisandverificationofit.Mobilepaymentprotocolisimplementedinamobileenvironment,andmobiledevicesarelimitedinpower,computingpowerandstoragespace,thoseposednewchallengestoformalanalysis,modelingandve

8、rificationofmobilepaymentprotocol.Thus,formalanalysisandverificationofmobilepaymentprotocolhasimportant