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

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

项目编号： No.61300177

项目类型： 青年科学基金项目

立项/批准年度： 2014

项目学科： 自动化技术、计算机技术

项目作者： 张子剑

作者单位： 北京理工大学

项目金额： 23万元

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

中文关键词： 密钥协商；符号化分析；隐私保护；智能电网；云

英文摘要： 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 an

英文关键词： Key Exchange；Symbolic Analysis；Privacy Protection；Smart Grid；Cloud