A Probabilistic, Language-Based Security Analysis

基于语言的概率安全分析

• 批准号: 9800785
• 负责人: Andre Scedrov
• 金额: --
• 依托单位: University of Pennsylvania
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1998
• 资助国家: 美国
• 起止时间: 1998-08-01 至 2002-01-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9800785&HistoricalAwards=false
• 关键词: Probabilistic; Language; Based; Security; Analysis

9800785 This proposal concerns links between programming language theory and semantics and probabilistic computation, with applications to security analysis. The proposed work is to develop an analysis of cryptographic protocols based on programming languages, but using the probabilistic techniques of cryptography. This is a departure from most formal analyses of cryptographic protocols, which treat cryptographic operations as "black boxes". The proposed work will include the development of a modal-typed, concurrent programming language for defining communicating systems of probabilistic polynomial-time processes. A novel property of the proposed language is the use of probabilistic rather than nondeterministic scheduling of processes. A related notion of observational equivalence for sets of probabilistic processes will play a central role in reasoning about this language and in its applications to security analysis. The proposed research will develop methods for reasoning about observational equivalence (or some approximation to observational equivalence such as probabilistic trace equivalence or bisimulation) and use these methods to establish security properties of various protocols. The proposed framework will provide a useful analysis tool for working backwards from security properties of a protocol to derive necessary properties of underlying encryption primitives.***

9800785这项建议涉及程序设计语言理论和语义学与概率计算之间的联系，以及在安全分析方面的应用。建议的工作是基于编程语言，但使用密码学的概率技术来开发密码协议的分析。这与大多数对密码协议的正式分析不同，后者将密码操作视为“黑匣子”。拟议的工作将包括开发一种模式型并发编程语言，用于定义概率多项式时间过程的通信系统。该语言的一个新特性是使用了进程的概率调度而不是不确定性调度。概率过程集的观测等价性的相关概念将在关于这种语言的推理及其在安全分析中的应用中发挥核心作用。所提出的研究将开发关于观测等价(或某种近似观测等价，例如概率迹等价或互模拟)的推理方法，并使用这些方法来建立各种协议的安全性质。建议的框架将提供一个有用的分析工具，用于从协议的安全属性向后工作，以推导出底层加密原语的必要属性。