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

Bruno Blanchet

Description

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].

• when


• security properties


• storage


• file system


• has focused


• event has


• proverif


• access control


• ac- cess control


• lockbox key

Sujets

• Blanchet
• Storage
• File system
• ProVerif
• Access control

Informations

• Publié par: profil-zyak-2012
• Nombre de lectures: 17
• Langue: English

Extrait

AutomatedFormalAnalysisofa ProtocolforSecureFileSharingonUntrustedStorage BrunoBlanchetAvikChaudhuri CNRS,E ´ coleNormaleSupe´rieure,INRIA ∗ UniversityofCaliforniaatSantaCruz [e-mail] [e-mail] Abstract Westudyformalsecuritypropertiesofastate-of-the-art protocolforsecurefilesharingonuntrustedstorage,inthe automaticprotocolverifierProVerif.Asfarasweknow, thisisthefirstautomatedformalanalysisofasecurestor- ageprotocol.Theprotocol,designedasthebasisforthe filesystemPlutus,featuresanumberofinterestingschemes likelazyrevocationandkeyrotation.Theseschemesim- provetheprotocol’sperformance,butcomplicateitssecu- rityproperties.Ouranalysisclarifiesseveralambiguities inthedesignandrevealssomeunknownattacksonthepro- tocol.Weproposecorrections,andproveprecisesecurity guaranteesforthecorrectedprotocol. 1.Introduction Muchresearchinrecentyearshasfocusedonthesecu- rityanalysisofcommunicationprotocols.Insomecases, attackshavebeenfoundonold,seeminglyrobustproto- cols,andtheseprotocolshavebeencorrected[23,33,40];in othercases,thesecurityguaranteesofthoseprotocolshave beenfoundtobemisunderstood,andtheyhavebeenclari- fiedandsometimesevenformalizedandproved[4,33,37]. Moregenerally,thislineofworkhasunderlinedthediffi- cultyofdesigningsecurecommunicationprotocols,andthe importanceofverifyingtheirprecisesecurityproperties. Whileprotocolsforsecurecommunicationhavebeen studiedindepth,protocolsforsecurestoragehavereceived farlessattention.Someoftheseprotocolsrelyonsecure communication,andweexpecttheusualtechniquesforse- curecommunicationtoapplytosuchprotocolsaswell.But somedistinctivefeaturesofstorageposeproblemsforse- curitythatseemtogobeyondthosestudiedinthecon- textofcommunicationprotocols.Perhapsthemoststrik- ingofthesefeaturesisdynamicaccesscontrol.Indeed, ∗ BrunoBlanchet’sworkhasbeendonewithintheINRIAABSTRAC- TIONproject-team(commonwiththeCNRSandtheE ´ NS). whilemoststoragesystemsfeaturedynamicaccesscontrol insomeform,itsconsequencesonmoreabstractsecurity propertieslikesecrecyandintegrityareseldomevaluated indetail. Inthispaper,weshowthatprotocolsforsecurestor- ageareworthanalyzing,andstudyaninterestingexample. Specifically,weanalyzeastate-of-the-artfile-sharingproto- colthatexploitscryptographictechniquesforsecurestorage onanuntrustedserver.Theprotocolisthebasisforthefile systemPlutus[32].Thissettingisinterestingforseveral reasons.First,compromiseofstorageserversisareason- ablycommonthreattoday,anditisprudentnottotrustsuch serversforsecurity[34].Next,theprotocolwestudyhasa verytypicaldesignforsecurefilesharingonuntrustedstor- age,wheredataisstoredencryptedandsigned,andkeys forencrypting,signing,verifying,anddecryptingsuchdata aremanagedbyusers.Severalfilesystemsfollowthisbasic design,includingSNAD[35],SiRiUS[28],andothercryp- tographicfilesystemssincethe1990s[15].Finally,beyond thebasicdesign,theprotocolfeaturessomepromisingnew schemeslikelazyrevocationandkeyrotationthatimprove theprotocol’sperformanceinthepresenceofdynamicac- cesscontrol,butinturncomplicateitssecurityproperties. Thesefeaturesareworthyofstudy.Forinstance,ouranaly- sisrevealsthatlazyrevocationallowsmorepreciseintegrity guaranteesthanthenaı¨veschemein[28].Withlazyrevo- cation,ifanuntrustedwriterisrevoked,readerscandis- tinguishcontentsthatarewrittenaftertherevocationfrom previouscontentsthatmayhavebeenwrittenbythatwriter; consequently,theycantrusttheformercontentsevenifthey donottrustthelattercontents.Onadifferentnote,thecom- putationalsecurityofkeyrotationschemeshasgenerateda lotofinterestrecently[6,7,26].Ouranalysisrevealssome newintegrityvulnerabilitiesintheprotocolthatcanbeex- ploitedevenifthekeyrotationschemeissecure. Formaltechniquesplayasignificantroleinouranalysis. Wemodeltheprotocolandverifyitssecuritypropertiesin theautomaticprotocolverifierProVerif.ProVerifisbased onsolidformalfoundationsthatincludetheoryfortheap- pliedpicalculusandprooftheoryforfirst-orderlogic.The