University of Cambridge > Talks.cam > Semantics Lunch (Computer Laboratory) > Reliable evidence: Auditability by typing

Reliable evidence: Auditability by typing

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2021 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity