Automatic Formal Analysis of a Protocol for Secure File Sharing on Untrusted Storage

Bruno Blanchet and Avik Chaudhuri

Abstract
We study formal security properties of a state-of-the-art protocol for secure file sharing on untrusted storage, in the automatic protocol verifier ProVerif. As far as we know, this is the first automated formal analysis of a secure storage protocol. The protocol, designed as the basis for the file system Plutus, features a number of interesting schemes like lazy revocation and key rotation. These schemes improve the protocol's performance, but complicate its security properties. Our analysis clarifies several ambiguities in the design and reveals some unknown attacks on the protocol. We propose corrections, and prove precise security guarantees for the corrected protocol.

PDF

BibTeX


@inproceedings{afapsfsus-BC08,

    
author = {Bruno Blanchet and Avik Chaudhuri},

    
title = {Automated Formal Analysis of a Protocol for Secure File
Sharing on Untrusted Storage},

    
booktitle = {Proceedings of the 29th IEEE Symposium on Security and Privacy (S&P'08)},

    
year = {2008},

    
pages = {417-431},

    
publisher = {IEEE}

}

OCaml generators for ProVerif models of Plutus
Download OCaml
Models without server-verified writes (Usage: plutusgen.exe -options max_rev; Options: plutusgen.exe -help)
Models with server-verified writes (Usage: plutusgenSVW.exe -options max_rev; Options: plutusgenSVW.exe -help)

Download ProVerif
A shell script to generate and test models

Some models that appear in the paper
The basic model in Theorems 4.4 and 4.6, for max_rev=1
The model with fix F in Theorem 4.7, for max_rev=1
The model with fix F and server-verified writes in Theorem 4.9, for max_rev=1
The flawed model with unchanged modulus in Section 4.3.1, for max_rev=1
The flawed model with unchanged token in Section 4.3.2, for max_rev=1