Award Abstract #0430594
Collaborative research: High-Fidelity Methods for Security Protocols

NSF Org:	CNS Division of Computer and Network Systems
Initial Amendment Date:	September 17, 2004
Latest Amendment Date:	August 26, 2008
Award Number:	0430594
Award Instrument:	Continuing grant
Program Manager:	Karl N. Levitt CNS Division of Computer and Network Systems CSE Directorate for Computer & Information Science & Engineering
Start Date:	October 1, 2004
Expires:	September 30, 2009 (Estimated)
Awarded Amount to Date:	$410000
Investigator(s):	John C. Mitchell mitchell@cs.stanford.edu (Principal Investigator)
Sponsor:	Stanford University 340 Panama Street STANFORD, CA 94305 650/723-2300
NSF Program(s):	ITR-CYBERTRUST
Field Application(s):	0000912 Computer Science
Program Reference Code(s):	HPCC,9218,7254
Program Element Code(s):	7456

ABSTRACT

Proposal Number: 0430594, 0429689, 0430076, 0430595



TITLE: Collaborative Research: High-Fidelity Methods for Security Protocols

PI: John Mitchell, Andre Scedrov, Vitaly Shmatikov, Daniele Micciancio

The design and security analysis of protocols that use cryptographic primitives is one of the most fundamental and challenging areas of computer security research. This project focuses on three topics: foundations of protocol analysis, automated tools, and application of tools and methods to selected protocols. Foundational work centers on relating and combining two previously separate approaches: logical methods based on symbolic execution of protocols, and computational methods involving probability and polynomial-time. The symbolic approach uses a highly idealized representation of cryptographic primitives and has been a successful basis for automated tools. Conversely, the computational approach yields more insight into the strength and vulnerabilities of protocols, but is difficult to apply and only accessible to a small number of true experts in the field. Building on past success using several automated tools, the project will devise tool-based methods that leverage new scientific foundations. Three likely application areas are secure group communication and key agreement protocols, schemes for privacy-preserving computations, and wireless networking and applications. In each of these areas, there is current demand for new secure protocols from user communities, there is ongoing activity in the research and standardization communities, and the value of combining symbolic and computational analysis concepts is evident.

PUBLICATIONS PRODUCED AS A RESULT OF THIS RESEARCH

(Showing: 1 - 6 of 6).

A. Datta, A. Derek, J. C. Mitchell, D. Pavlovic.  "A Derivation System and Compositional Logic for Security Protocols,"  Journal of Computer Security (Special Issue of Selected Papers from CSFW-16),  v.13,  2005,  p. 423.

A. Datta, A. Derek, J.C. Mitchell, V. Shmatikov, and M. Turuani.  "Probabilistic polynomial-time semantics for a protocol security logic,"  32nd International Colloquium on Automata, Languages and Programming (ICALP '05),  2005,  p. 16.

Anupam Datta, Ante Derek, John C. Mitchell and Arnab Roy.  "Protocol Composition Logic,"  Electronic Notes in Theoretical Computer Science,  v.172,  2007, 

Arnab Roy, Anupam Datta, Ante Derek, John C. Mitchell, Jean-Pierre Seifert.  "Secrecy Analysis in Protocol Composition Logic,"  11th Annual Asian Computing Science Conference,  2006, 

C. He, M. Sundararajan, A. Datta, A. Derek, J. C. Mitchell.  "A Modular Correctness Proof of TLS and IEEE 802.11i,"  ACM Conference on Computer and Communications Security (CCS '05),  2005,  p. 2.

M. Backes, A. Datta, A. Derek, J.C. Mitchell, and M. Turuani.  "Compositional Analysis of Contract Signing Protocols,"  18th IEEE Computer Security Foundations Workshop (CSFW '05),  2005,  p. 94.


(Showing: 1 - 6 of 6).

Please report errors in award information by writing to: awardsearch@nsf.gov.