在移动通信技术和网络迅速发展的今天，移动商务成为一个必然趋势。安全公平的移动交易成为学者们研究的焦点，而移动商务协议作为移动商务安全技术的应用服务层，安全性越来越引起人们的关注。着色Petri网(CPN)是一种高级的Petri网成功应用于通信协议和工作流的分析，目前使用CPN对移动商务协议进行属性分析的报道比较少。本文提出一种基于CPN的移动商务协议建模和安全属性分析的新方法，基于分析获得的安全移动商务协议特性设计了一个满足安全属性的新移动商务协议，并模拟实现了该协议，通过攻击验证了协议的安全性。本文首先介绍了移动商务协议研究现状和基本安全属性，以及目前分析方法中存在的问题。然后详细介绍了协议分析工具—着色Petri网及其仿真工具CPN Tools和分析方法。其次，本文提出了一个利用着色Petri网对移动商务协议进行建模的新方法，以典型的移动商务协议KSL为例，详细介绍了利用着色Petri网对协议安全属性的形式化分析方法，证明了方法的可行性和正确性，并发现了基于逻辑的形式化方法未能发现的可追究性上的缺陷。之后，通过逻辑分析验证了CPN方法能够发现成功新的协议漏洞，并总结概括出一般移动商务协议满足安全属性的必要条件。最后，基于上文的安全移动商务协议必要条件，提出新的移动商务协议，包括双向身份认证和移动宏支付协议两部分。并设计了一个移动商务系统实现该协议，经过仿真模拟攻击验证了协议满足认证性、完整性、私密性、不可否认性、可追究性和公平性，而且不会影响系统的传输速度。