![[Search]](/static/images/search.gif){kind=small}
![[A-Z Index]](/static/images/az.gif){kind=small}
![[Contact]](/static/images/contact.gif){kind=small}
![[University of Cambridge]](/static/images/identifier2.gif){kind=small}
![[Talks.cam]](/static/images/talkslogosmall.gif)
Nataliya Guts (visiting from INRIA)
Monday 15 June 2009, 12:45-14:00
Reliable evidence: Auditability by typing
- đ¤ Speaker: Nataliya Guts (visiting from INRIA)
- đ Date & Time: Monday 15 June 2009, 12:45 - 14:00
- đ Venue: Room FW26, Computer Laboratory, William Gates Building
Questions? Contact
Sam Staton
Abstract
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.
Series This talk is part of the Semantics Lunch (Computer Laboratory) series.
Included in Lists
- All Talks (aka the CURE list)
- bld31
- Cambridge talks
- Department of Computer Science and Technology talks and seminars
- Interested Talks
- Martin's interesting talks
- Room FW26, Computer Laboratory, William Gates Building
- School of Technology
- Semantics Lunch (Computer Laboratory)
- Trust & Technology Initiative - interesting events
- yk373's list
- yk449
Note: Ex-directory lists are not shown.