[Colloquium] Reminder: today's talk by Vitaly Shmatikov, SRI International
Margery Ishmael
marge at cs.uchicago.edu
Fri Feb 27 09:27:59 CST 2004
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.
More information about the Colloquium
mailing list