本论文分为七章，涉及三大研究部分：基础理论部分，安全协议部分，以及安全协议形式化分析部分。主要工作及研究结果如下： 在基础理论部分：(1)介绍了为适应Internet通信安全新需求而出现的数字签名方案：(2)探讨了安全电子认证中心CA在电子商务中的应用。 在安全协议部分：(3)明确给出了安全协议的定义、分类、性质、设计原则以及可能存在的缺陷；(4)分析了IKE协议的多种运行模式的原理，并在此基础上全面分析了其可能遭受的安全威胁；(5)综述了安全协议形式化分析的研究状况；(6)提出了对现有的安全协议形式化分析方法的分类，并分析了其所面临的新问题。 在安全协议形式化分析部分：(7)比较和分析了多种逻辑系统的特点并论述了其相互间的关系；(8)提出了能够更好地反映Timed-release公钥协议特性的CS逻辑的扩展逻辑，并对一个具体的协议实例给出了完整有效的形式化分析；(9)运用SVO逻辑对一个非否认协议实例进行了有效的形式化分析，并对协议的缺陷进行了改进；(10)明确了现行的基于攻击结构性方法的分类；(11)提出了一种验证主体双向认证的模型检测机制；(12)在分析模型检测技术和逻辑推证技术的优点与不足的基础上提出了一种混合的安全协议形式化分析方法，该方法可提供更为完全的安全协议形式化分析结果；(13)综述了多种基于证明结构性方法的原理；(14)给出了应用于不同系统的不变式的概述；(15)分析了各种不变式生成技术之间的关系，进行了分类，并探讨了不变式生成技术的未来发展趋势。