Advances in Language-Based Security Analysis

University Of Pennsylvania, Philadelphia PA

Investigators

Abstract

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.