This lab is about formal analysis. You will experience how to formally specify and verify a simple key management API using the tamarin prover.
- Prerequisites
- Task 1: key creation
- Task 2: encrypt and decrypt
- Task 3: wrap and unwrap
- Task 4: proof of security
This lab is inspired by the research paper:
Riccardo Focardi and Flaminia L. Luccio. 2021. A Formally Verified Configuration for Hardware Security Modules in the Cloud. In ACM CCS ’21. (official link, arxiv pdf)