BlanchetChaudhuriOakland08

Bruno Blanchet Back to publications
Bruno Blanchet and Avik Chaudhuri. Automated Formal Analysis of a Protocol for Secure File Sharing on Untrusted Storage. In IEEE Symposium on Security and Privacy, pages 417-431, Oakland, CA, May 2008. IEEE.

Copyright

© IEEE.

Get the paper

.pdf, 236 Kb

Links

ProVerif scripts available at http://www.soe.ucsc.edu/~avik/projects/plutus/

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.

Bibtex


@INPROCEEDINGS{BlanchetChaudhuriOakland08,
  AUTHOR = {Bruno Blanchet and Avik Chaudhuri},
  TITLE = {Automated Formal Analysis of a Protocol for Secure File Sharing on Untrusted Storage},
  BOOKTITLE = {IEEE Symposium on Security and Privacy},
  PAGES = {417--431},
  YEAR = 2008,
  ADDRESS = {Oakland, CA},
  MONTH = MAY,
  PUBLISHER = {IEEE}
}


E-mail/Courrier électronique : Bruno.Blanchet@trap-inria.fr (remove trap-)