Automated 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> maxrev; Options: plutusgen.exe -help)
 Models with server-verified writes (Usage: plutusgenSVW.exe -<options> maxrev; 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 maxrev=1
 The model with fix F in Theorem 4.7, for maxrev=1
 The model with fix F and server-verified writes in Theorem 4.9, for maxrev=1
 The flawed model with unchanged modulus in Section 4.3.1, for maxrev=1
 The flawed model with unchanged token in Section 4.3.2, for maxrev=1