[Colloquium] Vitaly Shmatikov on Friday, February 27, 2004

[Margery Ishmael]

DEPARTMENT OF COMPUTER SCIENCE - TALK

Date: Friday, February 27, 2004
Time: 2:30 p.m.
Place: Ryerson 251

-------------------------------------------

Speaker:  VITALY SHMATIKOV

From:  SRI International

Url:  http://www.csl.sri.com/users/shmat/

Title:  Formal analysis of security protocols: beyond Dolev-Yao

Abstract:

Security protocols are among the basic building blocks of distributed
computation, and are used for purposes as diverse as electronic 
commerce,
routing in ad-hoc networks and pay-per-view video broadcast.
Conventional formal verification methods for secure systems are based on
the idealized "Dolev-Yao" model, in which the underlying cryptographic
primitives are modeled as abstract data types.  This sacrifices
computational soundness of proofs of security, but enables automated
search for a large class of attacks.

In my talk, I will focus on systems and properties that cannot be 
analyzed
in the Dolev-Yao model, such as secure multicast and group key
distribution protocols.  I will describe the symbolic constraint solving
method which eliminates the need for a finite bound on the adversary. I
will then show how symbolic analysis is extended to account for 
algebraic
properties of cryptographic functions such as XOR and Diffie-Hellman
exponentiation, while preserving decidability.  In the second part of my
talk, I will discuss security properties involving discrete probability,
and describe some results in using probabilistic model checking to
discover flaws in anonymity systems based on randomized message routing.

-------------------------------------------------------

Host: DAVID B. MACQUEEN

*Refreshments will follow the talk in Ryerson 255*

People in need of assistance should call 773-834-8977 in advance.