Advances in Language-Based Security Analysis

基于语言的安全分析的进展

• 批准号: 0098096
• 负责人: Andre Scedrov
• 金额: $ 9.42万
• 依托单位: University of Pennsylvania
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2001
• 资助国家: 美国
• 起止时间: 2001-07-01 至 2005-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0098096&HistoricalAwards=false
• 关键词: Advances; Language; Based; Security; Analysis

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.

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