A Probabilistic, Language-Based Security Analysis

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

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.***