Automated Formal Analysis of a Protocol for Secure File Sharing on Untrusted Storage
15
pages
English
Documents
Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus
Découvre YouScribe et accède à tout notre catalogue !
Découvre YouScribe et accède à tout notre catalogue !
15
pages
English
Documents
Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus
Niveau: Supérieur, Doctorat, Bac+8
Automated Formal Analysis of a Protocol for Secure File Sharing on Untrusted Storage Bruno Blanchet CNRS, Ecole Normale Superieure, INRIA? Avik Chaudhuri University of California at Santa Cruz 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 stor- age 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 im- prove the protocol's performance, but complicate its secu- rity properties. Our analysis clarifies several ambiguities in the design and reveals some unknown attacks on the pro- tocol. We propose corrections, and prove precise security guarantees for the corrected protocol. 1. Introduction Much research in recent years has focused on the secu- rity analysis of communication protocols. In some cases, attacks have been found on old, seemingly robust proto- cols, and these protocols have been corrected [23, 33, 40]; in other cases, the security guarantees of those protocols have been found to be misunderstood, and they have been clari- fied and sometimes even formalized and proved [4, 33, 37].
Voir
Automated Formal Analysis of a Protocol for Secure File Sharing on Untrusted Storage Bruno Blanchet CNRS, Ecole Normale Superieure, INRIA? Avik Chaudhuri University of California at Santa Cruz 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 stor- age 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 im- prove the protocol's performance, but complicate its secu- rity properties. Our analysis clarifies several ambiguities in the design and reveals some unknown attacks on the pro- tocol. We propose corrections, and prove precise security guarantees for the corrected protocol. 1. Introduction Much research in recent years has focused on the secu- rity analysis of communication protocols. In some cases, attacks have been found on old, seemingly robust proto- cols, and these protocols have been corrected [23, 33, 40]; in other cases, the security guarantees of those protocols have been found to be misunderstood, and they have been clari- fied and sometimes even formalized and proved [4, 33, 37].
- when
- security properties
- storage
- file system
- has focused
- event has
- proverif
- access control
- ac- cess control
- lockbox key
Publié par
Langue
English
