SET协议形式化分析与模型检测

随着移动网络技术的快速发展,电子商务的大量普及,电子商务不在单单只是局限于有线网络,商家们开始将商机延续到移动网络。移动网络用户群体中手机移动上网用户占绝大部分,在这样的商机驱动下,移动电子商务得到快速发展。移动电子商务中最为核心的技术是移动电子支付协议SET,它直接决定了移动电子商务的安全性、高效性。本文就在这样的背景下采用AVISPA工具研究SET协议,通过形式化分析与模型检测,发现了SET协议的支付密钥的不安全性,并给出了攻击路径。

Formal Analysis and Model Checking of SET Protocol

With the rapid development of mobile network technology and a lot of popularity of electronic business,E-commerce is not just limited to cable network.The businesses will continue to develop mobile network.Phone mobile Internet users have the most group in mobile network users mobile,in such drive of business opportunities,mobile electronic business get fast development.The most core technology of mobile electronic business is the mobile electronic payment protocol SET,which directly determine the security and high efficiency of mobile e-business.In this paper I use the AVISPA tool to research SET protocol under this background,I found the security holes of SET protocol and give the attack path with formal analysis and model checking.