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.

Prerequisites

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

Usage

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