May 18, 2008 to May 21, 2008
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SP.2008.12
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.
secure storage, lazy revocation, key rotation, cryptographic access control, automatic verification
Bruno Blanchet, Avik Chaudhuri, "Automated Formal Analysis of a Protocol for Secure File Sharing on Untrusted Storage", SP, 2008, 2012 IEEE Symposium on Security and Privacy, 2012 IEEE Symposium on Security and Privacy 2008, pp. 417-431, doi:10.1109/SP.2008.12