基于ProVerif的安全攻击仿真+源代码(3)
（3）认证密钥交换协议[2,9]。通过结合认证协议和密钥交换协议，设计出同时具有认证性和机密性两种属性的新协议，即认证密钥交换协议。其通信过程主要分为两个步骤，首先参与者通过运行协议相互确认对方身份，然后参与者通过挑战应答方式获得安全通信的会话密钥。此类协议在网络通信应用中十分广泛，常见的认证密钥交换协议有X.509协议[11]、IKE协议[9,13]、Kerberos认证协议[9]、DASS协议[9]。
（4）电子商务协议[9,12]。随着网上交易的日益频繁，电子商务协议在电子交易过程中发挥着关键作用。在电子商务协议中，协议的参与者代表进行商务交易的双方，其利益目标不尽相同。此类协议主要应用Hash 函数[13,14]和数字签名[14,15]等安全技术来达到相应安全目标，其中，公平性[9]是电子商务协议最为重要的安全属性，即协议应保证双方能够公平、公正地进行交易而不损害彼此的利益。SSL协议[9]和SET协议[9]是应用范围广泛且最常见的电子商务协议。
1.1.4 安全协议的安全属性
安全协议是网络信息安全的重要保障，为网络通信中信息的传输与处理提供各种安全服务。而安全协议的目标集则构成了安全协议的安全属性集。安全属性[6,8]主要包括机密性、认证性、完整性、不可否认性、公平性、匿名性、可用性和可追究性等。
下面简要介绍前四类应用较广泛的安全属性[6,10]。
（1） 机密性
机密性也称为秘密性或保密性，即保护协议中秘密消息不为攻击者所窃取。一般，我们将机密性考虑为防止攻击者能得到被加密的消息，即攻击者无法得到消息的真实内容。保密性实现的最直接有效的办法是“加密”。通常使用的加密体制又分为对称加密体制和非对称加密体制。消息通过加密算法的加密由可见的明文变成了密文，并且密文在不拥有密钥的情况下是不能被解密的，这样就实现了消息的保密性。
（2）认证性
认证是协议双方通过验证双方的动作是否匹配来验证认证性的正确性。根据认证的目的不同，可将认证划分为数据源认证和身份认证。在这里，本文只考虑身份认证。身份认证是协议双方通过运行协议来认证对方身份的正确性，一般用于面向连接的服务。身份认证又分为双向认证和单向认证，双向认证是指参与者双方相互进行身份认证，而单向身份认证则是由单方发起的认证。
（3）完整性(Integrity)。
完整性指数据在传输或存储的过程中不被篡改，其目的是保护数据不被攻击者任意的修改、删除或替代。实现完整性的常用方法是签名和封装，它们的主要思想是使用密码算法或哈希函数来产生明文的摘要信息并将其附在所传送的密文之后一起传送给接收方，接收方通过对比摘要和密文的匹配性来验证消息的完整性。
（4）不可否认性(Non-repudiation)。
不可否认性是电子商务协议的主要属性之一。在电子商务协议中，交互双方不一定都是诚实的用户，可能存在欺诈行为。在电子商务协议中，不可否认性指协议既能记录并证明协议中用户确实执行了某些步骤，又能判断这些证据的正确性。数字签名技术是保证协议满足不可否认性的最常用手段。
1.2 安全协议形式化分析
1.2.1 安全协形式化分析的概念
形式化分析方法[4,5,7]，指通过精确的数学描述和强大的形式推理工具来自动化推理问题的方法。形式化分析方法首先使用形式化描述语言对安全协议进行形式化建模，然后对安全协议所申明的安全属性进行形式化定义，安全属性通常形式化定义为逻辑公式或者相应的断言的形式。因此，安全协议的形式化分析就转换为依据逻辑推理来判断安全协议的形式化模型是否满足其安全属性所对应的逻辑公式或者断言[12,13]。