Sciweavers

SP
2008
IEEE

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

14 years 5 months ago
Automated Formal Analysis of a Protocol for Secure File Sharing on Untrusted Storage
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.
Bruno Blanchet, Avik Chaudhuri
Added 01 Jun 2010
Updated 01 Jun 2010
Type Conference
Year 2008
Where SP
Authors Bruno Blanchet, Avik Chaudhuri
Comments (0)