根据CNNIC(China Internet Network Information Center,中国互联网络信息中心)发布的“第37次中国互联网络发展状况统计报告”,2015年,42.7%的网民遭遇过网络安全问题。随着网络购物群体的不断增大,电子商务安全问题引起了消费者的广泛关注。2015年,我国网络购物用户规模达到4.13亿,同时,16.4%的消费者在网购过程中遭遇到过网络消费欺诈。由此可见,网络安全问题和交易安全问题是保证电子商务进一步发展的关键之所在。交易协议是交易安全问题的核心。本文从网络交易安全问题出发,选取主流电子商务B2C模式作为研究对象,通过模型检测方法对基于第三方支付平台的交易协议进行了形式化建模、分析和验证,以保证买家和商户之间完成安全、可靠的交易活动。其主要内容如下：1.介绍了课题背景、相关理论基础和采用形式化方法分析安全协议的发展过程以及研究现状。2.对B2C模式涉及到的电子商务交易协议进行了简要的分析,使用Promela语言形式化地描述了电子商务交易协议中涉及到的四个实体：买家、商户网站、第三方支付平台和银行。3.使用模型检测方法对B2C模式交易协议进行形式化验证,对交易协议进行抽象化建模,描述了电子商务交易协议的LTL性质,使用Spin的图形界面工具XSpin得到交易协议的运行轨迹,在此基础上分析目前B2C模式交易协议存在的潜在安全隐患。4.针对分析结果,提出了一种基于B2C模式的改进模型,增加了物流方和第三方隐私服务器两个实体,用于规范交易流程和保护买家隐私。