基于线空间模型的安全协议形式化分析

《基于线空间模型的安全协议形式化分析》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、东南大学博士学位论文基于线空间模型的安全协议形式化分析姓名：杨明申请学位级别：博士专业：计算机应用技术指导教师：罗军舟20070301ABSTRACTSecurityprotocols，alsocalledcryptographicprotocols，areprotocolsthatusecryptographytoauthenticateprincipals．distributekeysortrausaetelectronicbusiness．FortheircorrecUlessarethetheoreticalbasisofthesecurityforInte

2、ractapplicationsanddistributedsystems，theformalanalysishasbeenahotresearchtopicforalongtime．Theobjectsforformalanalysisaleprotocols’securitypropertiesincludingcorrespondence，secrecy,electroniccommercerelatednon—repudiation,fairnessandtimeliness．Theworkinthisdissertationonlyfocusesthefu

3、ndamentalsecurityproperties，i．e．correspondenceandsecrecy,Mostoftheexistingformalmethodsadopteitherthereasoningtechnologiessuchasbelieflogiesortheoremprovingtechnologiessuchasstareexploration,andfacetheproblemsofweakanalysispowerandstateexplosionpuzzlesrespectively．Tosolvetheproblems，on

4、eoftbenewtrendsoftheresearchesisthesynthesizingofdifferenttechniquesforbesteffects．Accordingtothis，anewmethodbasedonchallenge-responseisproposedinthisdissertation,whichappliesstrandspacemodelasunderlyingsemanticmodelandauthenticationlogic∞baSicanalysismethod．Someothertechniquesinvolved

5、byAthenaalgorithmandauthenticationtestsarealsoapplied．Thewholeworkincludesfourparts，笛establishmentofsemanticmodel，proposalofanalysismethod，designofautomaticanalysistool，demonstrationandapplicationsofthenewtheory．Strandspacemodelisapplied笛theunderlyingsemanticmodel．basedonwhichclearform

6、aldefinitionsofcorrespondenceandsecrecyaregiven．Theanalysisofsecrecyissplitintotwoparts—Explicit-Information—LeakageanalysisandImplicit-information—Leakageanalysis，whilethelatterisbuiltuponcorrespondenceanalysis．andthecorrespondenceisconcluded髂theexistencerelationshipofstrandsandtheagr

7、eementofstrandparameters．AnewmethodbasedOnthesemanticmodelandformaldefinitionsisproposedhere．whichsynthesizestheideaSofsomeexistingmethodsincludingauthenticationlogic，Athenaalgorithm,Authenticationtestsandete．SomecommonconceptsoftheseresearchessuchasFreshness,Uniqueorigination，Testsa