Thursday 15th August, Morning session
Ioana Boureanu, University of Surrey
BACKGROUND:
In this tutorial we will try to understand why it is hard to formally verify privacy-like properties, such as strong secrecy, anonymity, unlinkability or lack of information flow, in well-established models for formal analysis of cryptographic protocols. We will then see how to do some approximations of this verification in state-of-the-art tools for what is called Dolev-Yao protocol analysis, such as Tamarin and a new tool called Phoebe. Finally, if time allows, we will touch upon on what privacy analysis may mean in the “sister formalisms” for proving cryptographic protocols secure or private, that is in computational models and accompanying tools such as Squirrel.
PREPARATION:
Additional materials may be circulated nearer the day, but students are asked to install the following on their machines in advance:
Haskell (https://www.haskell.org/)
Tamarin prover (https://tamarin-prover.com/), the newest version is fine.
Squirrel prover installed (https://squirrel-prover.github.io/)
SPEAKER:
Ioana Boureanu is a professor in secure systems at the University of Surrey.
She is primarily interested in formal methods for security and privacy, provable security, and applied cryptography.
She is also the director of Surrey Centre for Cyber Security, one of UK’s Academic Centre of Excellence in Cyber Security Research.
More on her work can be found at people.itcarlson.com/ioana