Practice-Oriented Provable Security for Higher-Layer Protocols: Models, Analyses and Solutions

面向实践的高层协议可证明安全性：模型、分析和解决方案

• 批准号: 0208842
• 负责人: Phillip Rogaway
• 金额: --
• 依托单位: University of California-Davis
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2002
• 资助国家: 美国
• 起止时间: 2002-07-15 至 2007-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0208842&HistoricalAwards=false
• 关键词: Practice; Oriented; Provable; Security; Higher

This research is about using the "provable-security approach" in the design and analysis of high-level cryptographic protocols. The aim is to gain assurance for practical cryptographic schemes by finding the right definitions, and then using modern techniques (reductions and their concrete-security analysis) to analyze selected schemes. Specific problems to be investigated include: (1) Storing a user's private information on an untrusted server. Here one wants to store user data in such a way that the user can recover it by presenting a password, but an adversary must invest an amount of interaction proportional to the guessing-complexity of the password. (2) The authenticated-encryption scheme in SSH. Though the method used by SSH is not, in general, correct, the situation for SSH itself is far from clear. (3) Delegation of authority to a secondary signature key by a primary one. A well-known approach in security practice, the problem that this solution aims to solve is without any provable-security treatment. (4) Relating the "prescriptive" approach to formalizing authenticated key exchange and the simulation-based approach. (5) Moving to an enriched model of computation, an envelope model, to investigate authenticated key exchange. (6) A systematic investigation of the "game walking" approach to analyzing cryptographic scenarios. Here two adversarial views are compared by writing out a sequence of pseudocode "games" each of which may set some Boolean flag. One bounds the difference in adversarial views by bounding the probability that the flag gets set.

这项研究是关于在高级加密协议的设计和分析中使用“可证明的安全方法”。 目的是通过找到正确的定义，然后使用现代技术（降低及其具体安全分析）来分析选定的方案，从而获得实用密码方案的保证。 要研究的具体问题包括：（1）将用户的私人信息存储在不受信任的服务器上。 在这里，人们希望以用户可以通过显示密码来恢复它的方式来存储用户数据，但是对手必须投资与密码的猜测复杂性成比例的交互。 （2）SSH中的身份验证 - 加密方案。 尽管SSH使用的方法通常不是正确的，但SSH本身的情况远非清晰。 （3）将权威授予次要签名密钥。 一种众所周知的安全实践方法，该解决方案旨在解决的问题没有任何可证明的安全处理。 （4）将“规范性”方法联系起来，以形式化身份验证的密钥交换和基于仿真的方法。 （5）转到一个富集的计算模型，一种包络模型，以研究身份验证的钥匙交换。 （6）对分析加密场景的“游戏步行”方法的系统调查。在这里，通过写出一系列伪代码“游戏”来比较两种对抗视图。一个人通过界定标志设置的概率来界定对抗视图的差异。