[an error occurred while processing this directive] MSR Papers

MSR Papers

MSR Home Page

MSR 3

Logical foundations

The following two papers lay out the foundations of MSR 3 as a rewriting interpretation of a large fragment of linear logic. They differ in their technical development: the longer journal version takes a historical perspective and establishes MSR 3 through a series of intermediate logical formalisms; the technical report takes a more intuitive approach that is based on an alternative reading of the sequent rules of linear logic.

MSR 2

Implementation

This paper describes the formal elements underlying the implementation of MSR 2 into an extension of rewriting logic with dependent types, and eventually into the Maude untyped rewriting engine.

Specification of Kerberos V

The papers below summarize the outcomes of a project which used MSR 2 to specify and analyze the popular Kerberos 5 authentication protocol. The results of this analysis showed that the core Kerberos protocol is sound, but it also revealed a number of anomalies that led the IETF Kerberos Working Group to modify its public specification documents (see CSFW'02 and TCS'06 papers below). It also unveiled correct but dangerous behaviors in the cross-realm authentication semantics of Kerberos 5 (see WITS'05 paper). Most recently, the project exposed a serious attack on PKINIT, a popular extension of Kerberos 5: this led the IETF to modify the specifications of PKINIT and Microsoft to immediately issue a security update for all versions of Windows (see I&C'08 paper).

Foundational Studies about Security Protocols

The series of papers below leverage the type system of MSR 2 to study the concept of an attacker in a cryptographic protocol. The second introduces the notion of "data access specification" (DAS) rules and uses them to show that the standard Dolev-Yao attacker specification can emulate the actions of an arbitrary symbolic adversary, thereby providing a formal justification of its use in almost all automated tools. The first shows that the Dolev-Yao intruder rules can be automatically reconstructed from the DAS rules, and that the DAS rules can themselves be inferred from annotated typing declarations for the various message constructors.

Language Description

The papers below describe early designs of MSR 2 and give a number of examples. While the general idea is captured in these papers, it does not account for some of the extension that were added during the implementation phase (see above). An up-to-date formal specification of MSR 2 is almost complete.

MSR 1.0

Decidability of Protocol Verification

The two papers below, from which MSR originated, established the first undecidability results for crypto-protocol verification (more specifically of the secrecy problem). Since then this line of investigation has been picked up by numerous researchers who specialized our results to particular classes of protocols.

Relation to Other Formalisms

This initial version of MSR also proved to be a formidable neutral ground where to formally relate the major families of languages for expressing protocols: the papers below build bridges between MSR 1 and the popular strand spaces, process algebras, and linear logic. This formally justified the independent development of the CAPSL Intermediate Language, a middleware that allowed translating specifications written in the language of one verification tool to the language of another.

Attacker Models

This paper relies on MSR 1 to show that all attacks that can be mounted by a traditional Dolev-Yao intruder against common cryptographic protocols can be enacted by an apparently weaker "Machiavellian" adversary in which compromised principals will not share long-term secrets and will not send arbitrary messages. It also shows that a Dolev-Yao adversary composed of multiple compromised principals is attack-equivalent to an adversary consisting of a single dishonest principal who is only willing to produce messages in valid protocol form.

Quantitative Protocol Analysis

The traditional Dolev-Yao model of security limits attacks to "computationally feasible" operations. This paper depart from this model by exploring a small extension of MSR 1 that assigns a cost to protocol actions, both of the Dolev-Yao kind as well as non traditional forms such as computationally-hard operations, guessing, principal subversion, and failure. This quantitative approach enables evaluating protocol resilience to various forms of denial of service, guessing attacks, and resource limitation.

Last modified: Fri Dec 31, 10 [an error occurred while processing this directive]