目前,全球移动电子商务呈现异常强劲的势头,我国移动电子商务也在迅速发展。用户使用移动电子商务时最关心的是安全问题,而移动电子商务协议的安全是保证移动电子商务安全的一个重要方面。移动电子商务协议是一类特殊的电子商务协议,与传统电子商务协议相比,由于移动装置和无线网络的特点,移动电子商务协议的执行环境更为复杂,从而使其更容易存在安全缺陷,同时也为其形式化分析与设计带来了新的挑战。本文主要研究了移动电子商务协议(包括无线认证协议,因为无线认证协议是移动电子商务协议的基础)的模型检验分析与设计,所取得的主要研究成果有:(1)应用模型检验方法对无线认证协议Server-specific MAKEP进行分析,借助模型检验工具SMV,成功地找到了协议存在的认证性缺陷,并对该缺陷所产生的影响进行了讨论;(2)针对Server-specific MAKEP协议存在的认证性缺陷,给出了协议的一种改进,并对改进后的协议再次进行模型检验分析,分析结果表明协议达到了安全要求;(3)针对移动电子商务协议,提出了一种基于有限状态机的建模方法;应用该方法,以一个典型的移动支付协议KSL为例进行模型检验分析;在检测出协议存在的公平性缺陷之后,给出了协议的一种改进;(4)针对移动装置和无线网络的特点,设计了一种移动环境公平支付协议,并对协议的公平性、保密性、时间性等性质进行模型检验分析,验证了其可行性。