[Nrg-l] FW: Security analysis of network protocols, Anupam Datta

Azer Bestavros best at cs.bu.edu
Mon Nov 14 09:32:30 EST 2005


-----Original Message-----
From: Be Blackburn [mailto:be at theory.csail.mit.edu] 
Sent: Monday, November 14, 2005 7:47 AM
To: imbe at mit.edu
Subject: Security analysis of network protocols, Anupam Datta


Open to the Public

DATE:    FRIDAY, November 18, 2005
TIME:    10:30 a.m. - 12:00 noon
PLACE:   32-G575, Stata Center, 32 Vassar Street
TITLE:   ``Security analysis of network protocols''
BY:  	 Anupam Datta, Stanford University


In this talk, I will present PCL - a logic for proving security
properties of network protocols. Two central results for this logic
are a "composition theorem" and a "computational soundness
theorem". The composition theorem allows proofs of complex protocols
to be built up from proofs of their constituent sub-protocols. It is
formulated and proved by adapting ideas from the assume-guarantee
paradigm for reasoning about distributed systems. The computational
soundness theorem guarantees that, for a class of security properties
and protocols, axiomatic proofs in PCL carry the same meaning as
hand-proofs done by cryptographers.

The soundness proof uses standard proof techniques from cryptography,
in particular, complexity-theoretic reductions. PCL has been
successfully applied to a number of internet, wireless and mobile
network security protocols developed by the IEEE and IETF Working
Groups, in several cases identifying serious security vulnerabilities.

More information about the Nrg-l mailing list