Advances in Language-Based Security Analysis

这个项目涉及安全分析中编程语言理论和语义学以及形式化方法之间的联系，在两个建模细节层面上。1)协议符号化执行的多集重写框架(MSR)检测常见的协议错误。该项目研究MSR形式主义中的可达性决策问题，扩展了不等价性测试。MSR的形式化分析也被扩展到公平交换协议的性质。研究了MSR与安全pi-演算之间的关系。2)另一种方法基于编程语言理论的方法，但结合了密码学的概率技术，开发了对密码协议的分析。这种方法允许分析概率协议和概率加密。在这个方向上的拟议工作发展了关于概率观测等价性的推理的原则和证明规则。讨论了概率进程演算的基本问题，如演算的精确运算语义，以及在允许多项式迭代的扩展版本中建立进程执行的多项式上界。研究了微积分的一个信息论变体及其与MSR的关系。

This project concerns links between programming language theory and semantics and formal methods in security analysis, on two levels of modeling detail. 1) Multiset rewriting framework (MSR), in which protocol execution is carried out symbolically, detects common protocol errors. The project studies decision problems for reachability in the MSR formalism extended with disequality testing. MSR formal analysis is also extended to properties of fair exchange protocols. The relationship between MSR and the secure pi-calculus is investigated. 2)A different approach develops an analysis of cryptographic protocols based on the methods of programming language theory, but incorporating the probabilistic techniques of cryptography. This approach allows the analysis of probabilistic protocols and probabilistic encryption. The proposed work in this direction develops principles and proof rules for reasoning about probabilistic observational equivalence. Foundational questions about probabilistic process calculus are addressed, such as a precise operational semantics of the calculus and the establishment of polynomial upper bounds on process execution in an extended version of the calculus that allows polynomial iteration. An information-theoretic variant of the calculus and the relationship to MSR are investigated.