基于GSPM的安全协议性质检验及其工具实现

《基于GSPM的安全协议性质检验及其工具实现》由会员上传分享，免费在线阅读，更多相关内容在工程资料-天天文库。

1、上海交通大学硕士学位论文基于GSPM的安全协议性质检验及其工具实现姓名：庄庆申请学位级别：硕士专业：计算机软件与理论指导教师：傅育熙20071201THEVERIFICATIONOFSECURITYPROTOCOLBASEDONGSPMANDTHEIMPLEMENTATIONOFTHETOOLABSTRACTItisakeyproblemwhetherasecurityprotocolreachesthedesignedsecuritycriteriasincenetworktechnologiesdevelo

2、prapidly.Formalmethodsandautomatedtoolsareveryimportanttechniquestoguaranteethesecuritypropertiesandtheapplicationrequirements.GSPM(GenericSecurityProtocolModel)issuchamethod.ThisdissertationinvestigatesthepropertiesofsecurityprotocolbaseduponGSPM・Firstly,as

3、typeattackflawsaffectthetypesofthemessages;thetypepatternruledesignedinGSPMistoostricttosolvetypeattackflaws・Soanewsemantictypeattackhasbeenaddedintothemodel,whichmakesGSPMstrongenoughtodetectthisflaw.Secondly,wedesignsomealgorithmstoanalyzethesecurityprotoc

4、olbasedonGSPM,includingmessagededucingalgorithm,messagematchalgorithmandstate-searchalgorithm・LTL(LinearTemporalLogic)isintroducedtodenotethepropertyofsecurityprotocol,likeconfidentialityandauthentication.Averificationalgorithmisdesignedduetothecharacteristi

5、cofLTL・Finally,thisdissertationpresentstheimplementationofanautomaticverificationtoolbasedonGSPMandthealgorithmsmentionedabove・ThetoolreceivesprotocolsandsecurityobjectivesasinputandautomaticallytranslatesthemintoGSPMsyntaxtoapplyspecificcheckingrules.Thisdi

6、ssertationgivesananalysisoftheresultandperformance.Italsoshowstheusingflowofthetool.KEYWORDS：GSPM,formalmethod,securityproperty,flaw,tool上海交通大学学位论文原创性声明本人郑重声明：所呈交的学位论文，是本人在导师的指导下，独立进行研究工作所取得的成果。除文中已经注明引用的内容外，本论文不包含任何其他个人或集体已经发表或撰写过的作品成果。对本文的研究做出重要贡献的个人和集体，均已

7、在文中以明确方式标明。本人完全意识到本声明的法律结果由本人承担。学位论文作者签名：庄庆日期：2008年1月18日上海交通大学学位论文版权使用授权书本学位论文作者完全了解学校有关保留、使用学位论文的规定，同意学校保留并向国家有关部门或机构送交论文的复印件和电子版，允许论文被查阅和借阅。本人授权上海交通大学可以将本学位论文的全部或部分内容编入有关数据库进行检索，可以采用影印、缩印或扫描等复制手段保存和汇编本学位论文。保密口，在年解密后适用本授权书。本学位论文属于不保密I（请在以上方框内打“7”）学位论文作者签名：庄

8、庆指导教师签名：傅育熙日期：2008年1月18日日期:2008年01月18日第一章绪论1.1引言在当今的互联网络中，如何保证网络安全成了一门重要的课题［1］。网络技术不断应用到各行各业，无论是政府、军事机构的数据库访问，还是商业用途的网上银行、电子交易，都时时存在遭到黑客攻击的危险。因此，近年来，网络信息安全问题已越来越受到关注。近年来，安全协议越来越多地用于保护因特网上传送的各种交易