Presentations

The agenda is posted at http://www.csl.sri.com/csfw/csfw16.

Probabilistic noninterference through weak probabilistic bisimulation, Geoff Smith. He uses security typing and a Markov chain model to analyze information flow between threads in a simplified language, assuming uniform random scheduling, where the objective is to protect the distribution of execution times of "low" threads. The weakened bisimulation (called "lumpability" in older texts) ignores stuttering within a thread.

Secure contexts for confidential data, Bossi et al. In the tradition of Focardi/Gorrieri SPA (Security Process Algebra), with the P_BNDC definition of noninterference (persistent bisimulation nondeducibility on compositions). A secure context is an environment that hides its high-level interactions from low-level processes.

Observational determinism for concurrent program security, Zdancewic and Myers. Secure concurrent language \lambda^PAR_SEC with message passing. Synchronization uses join patterns as in the join calculus. Given a race-free condition, correct typing prevents scheduler-based timing channels.

Symbolic protocol analysis with products and Diffie-Hellman exponentiation, Millen and Shmatikov. Reduction of reachability, in principle, to solving a system of quadratic Diophantine equations.

A procedure for verifying security against type confusion attacks, Meadows. A type function tree is essentially a structural signature of a symbolic message, and "type confusion games" are a way of detecting type coercions an attacker might succeed at. Probabilities and partial fields are modeled. Application to GDOI.

Anonymity and information hiding in multiagent systems, Halpern and O'Neill. Example: Chaum's Dining Cryptographers problem (did one of us pay the bill?). Epistemic logic, emphasis on semantics, related to earlier work on noninterference.

Understanding SPKI/SDSI using first order logic, Li and Mitchell. Argues that the SPKI extension to SDSI, introducing name strings, is problematic and it is better to use an extension of the RT (Role-based Trust management) language, which has FOL semantics.

Panel: Free term algebras for protocol analysis: what are they missing? Millen, Meadows and Scedrov sampled some of the unusual contexts and purposes of security protocols that are not ordinarily addressed by Dolev-Yao-style formal models, such as oblivious transfer, parties with limited trust, and alternative idealizations of operators.

A derivation system for security protocols and its logical formalization, Datta, Derek, Mitchell, Pavlovic. Hoare-axiom-like system for combining protocol segments with properties like Diffie-Hellman key agreement and challenge-response. Illustrated by derivation of ISO-9798-3 protocol. Specifications are in "cord calculus" with temporal logic annotations.

Automatic validation of protocol narration, Bodei et al. A narration is a message list annotated with some action instructions. Semantics in a new process language LYSA, Spi calculus without channels. The automatic analysis is a kind of approximate static analysis for authentication.

On distributed security transactions that use secure transport protocols, Broadfoot and Lowe. Assumes a two-layer system, where the lower SSL-like transport layer provides two-way authentication. CSP analysis.

Using access control for secure information flow in a Java-like language, Banerjee and Naumann. Static permissions on classes, stack inspection. Typing rules guarantee an invariant that "low" fields and variables never hold "high" locations.

Type-based distributed access control, Chotia, Duggan, Vitek. Key-based decentralized label model, two-layer type-kind framework. Uses propagating discretionary labels where owner Pi specifies which principals Pj1, ..., Pjn may read or write an object. Supports delegation and relaxation ("declassification") of constraints.

Using first-order logic to reason about policies, Halpern and Weissman. Permission policies may be stated in a decidable subset of FOL that permits negation, if they are free of "bipolars" that introduce troublesome potentially contradictory ambiguity. XrML (for digital rights) unfortunately allows them.

On generalized authorization problems, Jha, Reps, Schwoon, Stubblebine. Representation of SPKI/SDSI certificates as pushdown-machine stack operation rules, where extended names go on the stack. Certificates can be weighted so that an authorization problem (chain discovery) can be given an efficient algorithm that prefers less "sensitive" solutions.

Identity-based key agreement protocols from pairings, Chen and Kudla. Weil and Tate pairings are bilinear operations on elliptic curve groups with Diffie-Hellman-like properties, used previously by Boneh for identity-based encryption (but not key agreement). The title says it all.

The Diffie-Hellman key-agreement scheme in the strand space model, Herzog. Proves that if a Diffie-Hellman abstraction DH(x,y) is added to the strand space message algebra, legal strands do not imply any computation that would be intractable given the usual Diffie-Hellman assumptions.

A computational analysis of the Needham-Schroeder-Lowe protocol, Warinschi. Shows that the NSL protocol, while formally secure, is not secure if encryption is implemented with a form of ElGamal. Generally, to ensure soundness of abstract "Dolev-Yao" verification of this protocol, the encryption can be IND-CCA (indistinguishability under chosen-ciphertext attack) secure, but IND-CPA (...chosen-plaintext...) is insufficient.

Panel: A tribute to Professor Roger Needham. Syverson, Gollman, and Meadows reminisced with quotes and management philosophy from Roger Needham. (His definition of serendipity: looking for a needle in a haystack and finding the farmer's daughter.)