Reliable evidence: Auditability by typing

Add to your list(s) Download to your calendar using vCal

• Nataliya Guts (visiting from INRIA)
• Monday 15 June 2009, 12:45-14:00
• Room FW26, Computer Laboratory, William Gates Building.

If you have a question about this talk, please contact Sam Staton.

Many protocols rely on audit trails to allow an impartial judge to verify a posteriori some property of a protocol run. However, in current practice the choice of what data to log is left to the programmer’s intuition, and there is no guarantee that it constitutes enough evidence.

We give a precise definition of auditability and we show how typechecking can be used to statically verify that a protocol always logs enough evidence. We apply our approach to several examples, including a full-scale auction-like protocol programmed in ML.

This is joint work with Cedric Fournet and Francesco Zappa Nardelli.

This talk is part of the Semantics Lunch (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Room FW26, Computer Laboratory, William Gates Building
• School of Technology
• Semantics Lunch (Computer Laboratory)
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.