Models and Proofs of Protocol Security: A Progress Report

Bruno Blanchet3

Description

Niveau: Supérieur, Doctorat, Bac+8
Models and Proofs of Protocol Security: A Progress Report Martın Abadi1,2, Bruno Blanchet3,4,5, and Hubert Comon-Lundh5,6,7 1 Microsoft Research, Silicon Valley 2 University of California, Santa Cruz 3 CNRS 4 Ecole Normale Superieure 5 INRIA 6 Ecole Normale Superieure de Cachan 7 Research Center for Information Security, Advanced Industrial Science and Technology Abstract. This paper discusses progress in the verification of security protocols. Focusing on a small, classic example, it stresses the use of program-like represen- tations of protocols, and their automatic analysis in symbolic and computational models. 1 Introduction As computer security has become a broad, rich field, rigorous models have been devel- oped for many policies and mechanisms. Sometimes these models have been the subject of formal proofs, even automated ones. The goal of this paper is to discuss some of the progress in this direction and some of the problems that remain. The paper focuses on the study of security protocols, a large, mature, and active area. It aims to offer an introduction and a partial perspective on this area, rather than a comprehensive survey. We explain notations, results, and tools informally, through the description of a basic example: a variant of the classic Wide-mouthed-frog pro- tocol [25].

• precisely has


• probabilistic encryption


• language such


• frog protocol


• pid then let


• contains


• protocols


• wide-mouthed-frog pro- tocol


• purpose programming

Sujets

• Microsoft
• Needham
• Probabilistic encryption
• Protocol

Informations

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

Extrait

ModelsandProofsofProtocolSecurity: AProgressReport Mart ´ nAbad 1 i ,2 ,BrunoBlanchet 3,4,5 ,andHubertComon-Lundh 5,6,7 1 MicrosoftResearch,SiliconValley 2 UniversityofCalifornia,SantaCruz 3SRNC 4E ´ coleNormaleSupe´rieure 5INRIA 6E ´ coleNormaleSupe´rieuredeCachan 7ResearchCenterforInformationSecurity,AdvancedIndustrialScienceandTechnology Abstract.Thispaperdiscussesprogressinthevericationofsecurityprotocols. Focusingonasmall,classicexample,itstressestheuseofprogram-likerepresen- tationsofprotocols,andtheirautomaticanalysisinsymbolicandcomputational models. 1Introduction Ascomputersecurityhasbecomeabroad,richeld,rigorousmodelshavebeendevel- opedformanypoliciesandmechanisms.Sometimesthesemodelshavebeenthesubject offormalproofs,evenautomatedones.Thegoalofthispaperistodiscusssomeofthe progressinthisdirectionandsomeoftheproblemsthatremain. Thepaperfocusesonthestudyofsecurityprotocols,alarge,mature,andactive area.Itaimstoofferanintroductionandapartialperspectiveonthisarea,ratherthan acomprehensivesurvey.Weexplainnotations,results,andtoolsinformally,through thedescriptionofabasicexample:avariantoftheclassicWide-mouthed-frogpro- tocol[25].Forthisexample,weconsiderspecicationsandautomatedproofsintwo formalisms.Wereferthereadertotheresearchliteratureforpresentationsofother formalismsandforprecisedenitionsandtheorems,andtoarecenttutorial[1]for additionalbackground. Currentresearchinthisareaaddressesatleastthreechallenges: 1.thetreatmentofrealistic,practicalprotocols; 2.theanalysisofactualimplementationcode; 3.extendingtheanalysistorenedmodels,inparticularcomputationalmodelswith complexity-theoretichypothesesoncryptographicfunctions. Withregardto(1),protocolanalysisappearstobecatchingupwithprotocoldevel- opment.Inthelastfewyearstherehavebeenincreasinglythoroughanalysesofprac- ticalprotocols.Whiletheseanalysesremainlaboriousanddifcult,thesophistication andpowerofthetechniquesandtoolsforprotocolanalysisseemtohavegrownfaster thanthecomplexityofpracticalprotocols.Forinstance,inthelastdozenyears,the