BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Reliable evidence: Auditability by typing - Nataliya Guts (visitin
 g from INRIA)
DTSTART:20090615T114500Z
DTEND:20090615T130000Z
UID:TALK18270@talks.cam.ac.uk
CONTACT:Sam Staton
DESCRIPTION:Many protocols rely on audit trails to allow an impartial judg
 e to verify a posteriori some property of a protocol run. However\, in cur
 rent practice the choice of what data to log is left to the programmer's i
 ntuition\, and there is no guarantee that it constitutes enough evidence.\
 n\nWe give a precise definition of auditability and we show how typechecki
 ng can be used to statically verify that a protocol always logs enough evi
 dence. We apply our approach to several examples\, including a full-scale 
 auction-like protocol programmed in ML.\n\nThis is joint work with Cedric 
 Fournet and Francesco Zappa Nardelli.
LOCATION:Room FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR