计算可靠且可组合安全的复杂密码协议符号化分析方法研究

The traditional symbolic analysis methods cannot maintain the computational soundness, because the specific security properties of the cryptographic algorithms have not been defined formally during the process of modeling. Meanwhile, since the modular approach of the cryptographic protocols have not been realized so far, the symbolic analysis cannot be decomposed from an entire cryptographic protocol to some cryptographic sub-protocols. Therefore, these methods cannot maintain the composable security as well. This leads that these methods are inefficiency because of the state space explosion problem, when analyzing a complex cryptographic protocol which is composed by different kinds of the cryptographic algorithms and the cryptographic sub-protocols. To design the symbolic analysis methods with computational soundness and composable security, so as to implement the correct and effective symbolic analysis of the complex cryptographic protocols, with the help of the computational soundness proof and the composable security proof of the symbolic analysis methods, we study as the following: 1) Design the extendable symbolic models of the cryptographic algorithms, which support different kinds of the crytographic algorithms simultaneously. Moreover, prove that these models preserve both the compuational soundness and the composable security. 2) Design the symbolic analysis methods of the complex cryptographic protocols. Furthermore, prove that these methods preserve both the computational soundness and the composable security as well. 3) Design and implement a verification platform for the cryptographic protocols, and check whether the symbolic analysis methods can realize both the correct and effective analysis of the complex cryptographic protocols. This research realizes the security analysis of the complex cryptographic protocols, and has significantly theoratical meaning and practical value.

传统的符号化分析方法因在建模过程中并未形式化定义密码算法所需满足的具体安全属性，所以不具有计算可靠性。同时，该方法因尚未实现协议的模块化分析技术，无法将分析完整的密码协议拆分成分析若干密码子协议，所以不具有可组合安全性。这导致该方法在分析由多种密码算法和密码子协议组成的复杂密码协议时，存在状态空间爆炸问题效率低。为设计兼具计算可靠性和可组合安全性的符号化分析方法，以正确且高效的分析复杂密码协议，本项目拟就如下工作展开研究：①设计同时支持多种密码算法的密码算法可扩展符号化模型，并证明其兼具计算可靠性和可组合安全性。②面向密码算法可扩展符号化模型，设计同时支持多种密码协议的复杂密码协议符号化分析方法，并证明其兼具计算可靠性和可组合安全性。③搭建协议安全性验证平台，验证设计的符号化分析方法能够正确且高效的分析复杂密码协议。本项目实现了复杂密码协议的安全性分析，具有重要的理论意义和应用价值。

本项目研究一种同时支持多种密码算法的密码算法可扩展符号化模型。在此基础上，研究同时支持多种密码协议的计算可靠且可组合安全的符号化分析方法,并搭建实验平台进行验证。.. 项目组利用设计的符号化分析方法分析了基于口令的跨域群组认证密钥协商协议，智能电网中基于可充放电电池的差分隐私保护方案和电表读数融合协议，群智感知中扰动压缩感知协议，外包云上智能电表数据隐私友好存储和安全审计协议，以及有效期有限的匿名视频订阅方案的安全性。上述工作表明，本项目提出的符号化分析方法具有一定的实用性。.. 项目执行期间，项目组共发表SCI论文7篇，EI论文3篇，申请国家发明专利2项，培养博士生3名，硕士生5名。完成了所有预期研究成果。