安全协议的安全性是网络安全的重要基础,运用形式化方法分析安全协议已成为目前研究的主要热点。本文主要研究运用形式化方法分析安全协议的理论与技术,对基于模型检测技术的运行模式分析法进行深入的研究,并把其扩展到公平交换协议的分析与设计中去。主要的研究成果如下:(1)介绍安全协议的背景及基本概念、研究进展和发展趋势,概述了安全协议的分类和安全协议的形式化分析方法的三种思路;(2)介绍两方和三方安全协议的运行模式分析法,设计并提出了两方乐观公平交换协议运行模式分析法;(3)使用运行模式分析法成功分析了几个电子商务协议,如SET协议、Micali的电子合同协议ECS1、FPH电子邮件协议,得到了较好的结论;(4)根据公平交换协议的特点,提出了公平交换协议的设计原则,并设计了一个安全的电子合同签署协议;