题目：计算可靠的安全协议符号分析方法研究

安全协议是解决网络安全问题最有效的手段之一。然而，由于互联网的开放性和协议的并发性，安全协议的设计和分析一直是一个复杂而困难的问题。实践证明，借助形式化的方法或工具分析安全协议是非常必要而且行之有效的。

安全协议的形式化分析已有三十多年的历史，一直存在两类不同的方法：计算方法和符号方法。计算方法是在概率论和计算复杂性理论基础上的一种“归约”方法，其结果更具密码学可靠性。但是证明过程是高度创造性的手工数学式证明，这对于目前越来越复杂的安全协议，不仅证明本身越来越复杂，而且证明的正确性也越来越不容易。符号方法用形式化语言和符号推理对协议进行分析和验证，更容易实现自动化分析。但是由于对密码学原语和攻击者能力的理想建模，使得这类分析方法的肯定性结论往往并不直接具有现实意义，被认为没有真正建立起密码学的可靠性。

因此，结合符号方法和计算方法的优点，得到既简洁易用、又具有计算可靠性的分析方法是安全协议形式化研究领域的研究焦点。沿着这个思路，本文为建立计算可靠的安全协议符号分析方法进行了以下几个方面的研究，取得了的一系列的研究成果：

1).不可区分属性的计算可靠性分析方法研究。提出了计算可靠且支持双线性对、对称加密以及密钥循环的安全协议符号模型，该模型明确指定双线性对实例生成器和加密算法需要满足的安全属性，并证明了在满足这些安全属性的条件下，符号方法分析的不可区分属性蕴含计算方法分析的不可区分属性，这保证了该模型具有计算可靠性。同时，该模型通过增强攻击者对密钥循环的控制能力去除了无密钥循环的限制。

2).踪迹属性的计算可靠性分析方法研究。在主动攻击者模型下，提出了计算可靠且支持双线性对、公钥加密、数字签名的安全协议符号模型，该模型明确指定双线性对实例生成器、加密算法和签名算法需要满足的安全假设，并证明了在满足这些安全假设的条件下，符号方法分析的踪迹属性蕴含计算方法分析的踪迹属性，这保证了该模型具有计算可靠性。

3).通用可复合符号分析方法研究。通过扩展现有通用可复合符号分析方法，使其可以分析基于双线性对的密钥交换协议，并在保证计算可靠性的同时，还可以保证可复合安全性。将符号模型中的密码学抽象操作与UC模型中的理想功能进行了结合，并且证明了如果协议在符号模型下满足了相应的安全性质，则在UC模型下一定安全的实现了相应的理想功能。

4).通用可复合符号分析方法分析密钥交换协议。利用本文扩展后的通用可复合符号分析方法分析了Joux、TAK和TAKC密钥交换协议的各种安全属性，验证了提出的方法可以支持基于双线性对、加密和签名的多方密钥交换，并且在使用的密码原语满足理想功能的条件下，分析结果具有计算可靠性。