Automated Formal Analysis of aProtocol for Secure File Sharing on Untrusted StorageBruno BlanchetCNRS,´Ecole Normale Sup´erieure, INRIA∗[email protected] ChaudhuriUniversity of California at Santa [email protected] study formal security properties of a state-of-the-artprotocol for secure file sharing on untrusted storage, in theautomatic 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 thefile system Plutus, features a number of interesting schemeslike lazy revocation and key rotation. These schemes im-prove the protocol’s performance, but complicate its secu-rity properties. Our analysis clarifies several ambiguitiesin the design and reveals some unknown attacks on the pro-tocol. We propose corrections, and prove precise securityguarantees for the corrected protocol.1. IntroductionMuch 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]; inother cases, the security guarantees of those protocols havebeen found to be misunderstood, and they have been clari-fied and sometimes even formalized and proved [4, 33, 37].More generally, this line of work has underlined the diffi-culty of designing secure communication protocols, and theimportance of verifying their precise security properties.While protocols for secure communication have beenstudied in depth, protocols for secure storage have receivedfar less attention. Some of these protocols rely on securecommunication, and we expect the usual techniques for se-cure communication to apply to such protocols as well. Butsome distinctive features of storage pose problems for se-curity that seem to go beyond those studied in the con-text of communication protocols. Perhaps the most strik-ing of these features is dynamic access control. Indeed,∗Bruno Blanchet’s work has been done within the INRIA ABSTRAC-TION project-team (common with the CNRS and the´ENS).while most storage systems feature dynamic access controlin some form, its consequences on more abstract securityproperties like secrecy and integrity are seldom evaluatedin detail.In this paper, we show that protocols for secure stor-age are worth analyzing, and study an interesting example.Specifically, we analyze a state-of-the-art file-sharing proto-col that exploits cryptographic techniques for secure storageon an untrusted server. The protocol is the basis for the filesystem Plutus [32]. This setting is interesting for severalreasons. First, compromise of storage servers is a reason-ably common threat today, and it is prudent not to trust suchservers for security [34]. Next, the protocol we study has avery typical design for secure file sharing on untrusted stor-age, where data is stored encrypted and signed, and keysfor encrypting, signing, verifying, and decrypting such dataare managed by users. Several file systems follow this basicdesign, including SNAD [35], SiRiUS [28], and other cryp-tographic file systems since the 1990s [15]. Finally, beyondthe basic design, the protocol features some promising newschemes like lazy revocation and key rotation that improvethe protocol’s performance in the presence of dynamic ac-cess control, but in turn complicate its security properties.These features are worthy of study. For instance, our analy-sis reveals that lazy revocation allows more precise integrityguarantees than the na¨ıve scheme in [28]. With lazy revo-cation, if an untrusted writer is revoked, readers can dis-tinguish contents that are written after the revocation fromprevious contents that may have been written by that writer;consequently, they can trust the former contents even if theydo not trust the latter contents. On a different note, the com-putational security of key rotation schemes has generated alot of interest recently [6, 7, 26]. Our analysis reveals somenew integrity vulnerabilities in the protocol that can be ex-ploited even if the key rotation scheme is secure.Formal techniques play a significant role in our analysis.We model the protocol and verify its security properties inthe automatic protocol verifier ProVerif. ProVerif is basedon solid formal foundations that include theory for the ap-plied pi calculus and proof theory for first-order logic. The2008 IEEE Symposium on Security and Privacy978-0-7695-3168-7 /08 $25.00 © 2008 IEEEDOI 10.1109/SP.2008.12417Authorized licensed use limited to: Purdue University. Downloaded on August 27, 2009 at 17:33 from IEEE Xplore. Restrictions apply.formal language forces us to specify the protocol precisely,and prove or disprove precise security properties of the pro-tocol. This level of rigor pays off in several ways:• We find a new integrity attack on the protocol, andshow that it can have serious practical consequences.That this attack has eluded discovery for more thanfour years is testimony to the difficulty of finding suchattacks “by hand”.• We propose a fix and prove that it corrects the proto-col. Both the attack and the correction are relative toa formal specification of integrity that is not immedi-ately apparent from the informal specification in [32].We also prove a weaker secrecy guarantee than the oneclaimed in [32] (and show that their claim cannot betrue).• The formal exercise allows us to notice and clarifysome ambiguities in [32]; it also allows us to find somenew, simpler attacks where more complex ones wereknown. These discoveries vastly improve our under-standing of the protocol’s subtleties.• Finally, the use of an automatic verifier yields a muchhigher level of confidence in our proofs than manualtechniques, which have been known to be error-prone.More generally, our results reconfirm that informal justifica-tions (such as showing resistance to specific attacks) are notsufficient for protocols. As far as we know, our study is thefirst automated formal analysis of a secure storage protocol;we expect our approach to be fruitful for other protocols inthis area.Related work There is a huge body of work on formalmethods for the verification of security protocols, e.g., [1,4, 8, 16, 29, 33, 37]. We refer the reader to [14] for more in-formation on this work, and we focus here on more closelyrelated work on the design and verification of secure filesystems.In file systems based on the