中文摘要：

随着通信网络的广泛应用，保障通讯安全的密码协议在应用中日趋复杂化。而大多数复杂协议通常由单功能协议复合而成。因此，如何建立形式化方法分析单功能的协议并且保证复杂协议的安全性，是当前密码协议分析领域的一个研究热点。在现有密码协议分析方法中，形式化方法对协议的通用可复合性支持较弱，且不保证计算可靠性；而基于可复合框架的方法可保证计算可靠性，但符号化和自动化程度较低，分析过程繁难复杂,难以掌握和应用。本项的目标是形成一套计算可靠的、通用可复合的符号化密码协议分析模型和方法。具备如下特点1)操作简洁协议分析完全在形式化模型下进行； 2) 计算可靠符号分析的安全性保证协议计算模型下的安全性；3)通用复合协议安全性在协议复合情况下仍然保持。该项目的研究将为日益复杂化的密码协议的安全性分析，提供一种简洁可靠，自动化程度高的分析手段。

结论摘要：

密码协议的分析是安全协议研究中的重要一环，是信息安全保障的一个重要而无法回避的关键问题，而大多数复杂的协议通常是由单功能协议复合而成，因此，如何建立分析单功能的协议并且保证复合后协议的安全性问题成为了当今密码研究中的一个热点问题。本项目对于各类复合密码协议的分析方法以及计算可靠性问题进行了系统、深入的理论研究、探讨与总结，提出了一些具有较广应用或者安全性较高的密码方案并进行了一定的安全性证明，如基于LWE问题的零知识证明协议的构造，随机应答器模型下IK-CPA与IE-CCA安全性之间的关系的讨论，在具体的密码协议使用过程中可能会出现的密钥相关消息安全性研究以及近年来比较热门的云计算、云存储和外包计算等问题。此外，还对一些具有实用性的安全协议(如单点登录协议等)的逻辑系统计算可靠性以及不安全性进行了详细的分析。