CloudHSM-model

This repository contains the Tamarin prover model that we used to specify and check the Cloud HSM secure configuration described in the paper:

R. Focardi and F. L. Luccio. A Formally Verified Configuration for Hardware Security Modules in the Cloud. ACM CCS 2021, November 2021. [Conference version and presentation][Author's version on arxiv]

Model

Currently, we make available two versions of the model:

The original Tamarin prover model from the CCS paper;
An updated Tamarin prover model with the following improvements with respect to the original model:
- We now use K(...) instead of KU(...) to model attacker knowledge in the three secrecy lemmas as KU is, in fact, Tamarin-internal. Lemmas are still proved automatically but the check is a bit slower (see below). Many thanks to Cas Cremers for spotting this.

To check the model you need to install the Tamarin prover.

The reported execution times were obtained on a 2018 MacBook pro.

The full model can be checked with Tamarin in about 1m50s (1m30s for the original model) as follows:

$ tamarin-prover --prove HSM_model_CCS_updated.spthy

The full model includes one helper lemma used to make the proof converge (named Unwrap) and a number of sanity lemmas.

Checking just the secrecy lemmas takes about 1m (22s for the original model):

$ tamarin-prover --prove=Secrecy* HSM_model_CCS_updated.spthy

Checking just the Unwrap helper lemma takes about 1m04s:

$ tamarin-prover --prove=Unwrap HSM_model_CCS_updated.spthy