Advances in Language-Based Security Analysis

该项目涉及编程语言理论与语义和形式化方法在安全分析中的联系，涉及两个层次的建模细节。1)多集重写框架（Multiset rewrite framework， MSR），以符号方式执行协议，检测常见的协议错误。本课题研究了带不等式检验扩展的MSR形式下的可达性决策问题。MSR形式化分析也扩展到公平交换协议的性质。研究了安全系数与安全系数之间的关系。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.