随着网络通信技术的发展,电子商务已经渗透到人们的日常生活当中。特别是3G时代的到来,使移动商务得到了快速的发展。而移动商务协议的安全性是制约移动商务发展的主要瓶颈,这其中主要包括两个方面:一方面是负责交易双方身份认证的移动认证协议的安全性；另一方面是负责安全有效支付的移动支付协议的安全性。所以,运用形式化分析方法分析这两方面协议以及协议整体的安全性对于保障一个电子商务系统的安全运行尤为重要。目前,现有的形式化方法对于分析移动商务协议都具有一定的局限性,仅能分析部分子协议,而不能对包含多个子协议的复杂协议进行全面的分析。更重要的是,移动环境与有线网络相比更为复杂,并有其自身的特点,一些特点在现有形式化方法中并没有被合理的考虑,因此有必要结合不同形式化方法的优点,并找到一种更为严谨、全面而有效的形式化方法来分析移动商务协议的安全性。　　 本文结合定理证明的串空间理论、模态逻辑的卿逻辑和PCL组合逻辑这三种形式化方法,通过扩展它们的分析能力,分别提出了分析移动认证子协议和移动支付子协议安全性的方法,以及分析移动商务协议整体安全性的组合验证方法。主要工作内容包括:　　 首先,针对移动认证协议在设计过程中往往因考虑效率问题而使用了较低安全级别的密码算法,进而导致协议漏洞的安全问题,通过扩展串空间模型,形式化描述了一种常见的情形并提出了利用串空间模型验证移动身份认证协议安全性的一般性方法,并分别以Linear MAKEP无线认证协议和国际新标准IEEE802.16e-2005中的XH—PKMv2认证协议为例,分析了他们的安全属性,发现Linear MAKEP协议不满足认证性和验证了XH-PKMv2协议是正确的,得出了与国内外学者用其他形式化方法分析相同的结论,进而验证了此方法的有效性。在此基础上,针对Linear MAKEP协议的缺陷进行了改进,提出了一个更安全的增强型Enhance Linear MAKEP认证协议(ELM),并对改进后的协议进行了形式化验证。　　 其次,针对移动商务协议在复杂的移动环境中需要满足多种安全属性的问题,对卿逻辑进行了扩展,并提出了利用扩展后的卿逻辑分析移动支付协议几种安全属性的方法,并分别以著名的ISI在线支付协议和FMPP乐观移动支付协议为例,分析了他们的安全属性,发现了ISI协议不满足原子性和验证了FMPP协议的设计目标,进而验证了此方法的有效性。在此基础上,针对ISI支付协议的缺陷进行了改进,提出了一个更安全的增强型Enhance ISI支付协议(EISI)。　　 最后,基于DDMP协议组合分析模型设计了由ELM协议和EISI协议两个子协议组成的完整的移动商务协议,并给出了ELM协议模块化的演绎过程。利用PCL协议组合逻辑对所设计的移动商务协议整体安全性进行了形式化验证。结果表明组成后的ELMISI移动商务协议满足秘密性、认证性、可追究性、公平性及原子性。