Mark Ryan, University of Birmingham

Verifying real-life protocols: theory and two case studies

We use the applied pi calculus (a derivative of the pi calculus), and
a tool called ProVerif that supports it, to prove security properties
of systems. I will outline the developments of the method and the tool
for two case studies.

1. The Trusted Platform Module (TPM) is a hardware chip designed to
give greater security to laptops and desktops than is possible in
software alone. The TPM has registers called platform configuration
registers (PCRs), which are registers for maintaining state inside the
TPM. We show how to reason with such systems that have persistent
state.

2.  Cloud computing means entrusting data to information systems that
are managed by external parties on remote servers, in the "cloud",
raising new privacy and confidentiality concerns. We focus on the
particular cloud computing application of conference management. We
identify the specific security and privacy risks that existing systems
like EasyChair and EDAS pose, and address them with a protocol
underlying a novel cloud-based conference management system that
offers strong security and privacy guarantees. We prove that the
privacy properties hold.

This work brings together work I have done with several collaborators:
M. Arapinis, S. Bursuc, S. Delaune, S. Kremer, E. Ritter, and
G. Steel.