15 Pages
English

Models and Proofs of Protocol Security: A Progress Report

-

Gain access to the library to view online
Learn more

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


Subjects

Informations

Published by
Reads 17
Language English
ModelsandProofsofProtocolSecurity:AProgressReportMart´nAbad1i,2,BrunoBlanchet3,4,5,andHubertComon-Lundh5,6,71MicrosoftResearch,SiliconValley2UniversityofCalifornia,SantaCruz3SRNC4E´coleNormaleSupe´rieure5INRIA6E´coleNormaleSupe´rieuredeCachan7ResearchCenterforInformationSecurity,AdvancedIndustrialScienceandTechnologyAbstract.Thispaperdiscussesprogressinthevericationofsecurityprotocols.Focusingonasmall,classicexample,itstressestheuseofprogram-likerepresen-tationsofprotocols,andtheirautomaticanalysisinsymbolicandcomputationalmodels.1IntroductionAscomputersecurityhasbecomeabroad,richeld,rigorousmodelshavebeendevel-opedformanypoliciesandmechanisms.Sometimesthesemodelshavebeenthesubjectofformalproofs,evenautomatedones.Thegoalofthispaperistodiscusssomeoftheprogressinthisdirectionandsomeoftheproblemsthatremain.Thepaperfocusesonthestudyofsecurityprotocols,alarge,mature,andactivearea.Itaimstoofferanintroductionandapartialperspectiveonthisarea,ratherthanacomprehensivesurvey.Weexplainnotations,results,andtoolsinformally,throughthedescriptionofabasicexample:avariantoftheclassicWide-mouthed-frogpro-tocol[25].Forthisexample,weconsiderspecicationsandautomatedproofsintwoformalisms.Wereferthereadertotheresearchliteratureforpresentationsofotherformalismsandforprecisedenitionsandtheorems,andtoarecenttutorial[1]foradditionalbackground.Currentresearchinthisareaaddressesatleastthreechallenges:1.thetreatmentofrealistic,practicalprotocols;2.theanalysisofactualimplementationcode;3.extendingtheanalysistorenedmodels,inparticularcomputationalmodelswithcomplexity-theoretichypothesesoncryptographicfunctions.Withregardto(1),protocolanalysisappearstobecatchingupwithprotocoldevel-opment.Inthelastfewyearstherehavebeenincreasinglythoroughanalysesofprac-ticalprotocols.Whiletheseanalysesremainlaboriousanddifcult,thesophisticationandpowerofthetechniquesandtoolsforprotocolanalysisseemtohavegrownfasterthanthecomplexityofpracticalprotocols.Forinstance,inthelastdozenyears,the