安全協(xié)議進(jìn)化生成與模態(tài)邏輯驗(yàn)證研究

ID:36354553

大?。?.83 MB

頁(yè)數(shù):138頁(yè)

時(shí)間:2019-05-10

安全協(xié)議進(jìn)化生成與模態(tài)邏輯驗(yàn)證研究_第1頁(yè)
安全協(xié)議進(jìn)化生成與模態(tài)邏輯驗(yàn)證研究_第2頁(yè)
安全協(xié)議進(jìn)化生成與模態(tài)邏輯驗(yàn)證研究_第3頁(yè)
安全協(xié)議進(jìn)化生成與模態(tài)邏輯驗(yàn)證研究_第4頁(yè)
安全協(xié)議進(jìn)化生成與模態(tài)邏輯驗(yàn)證研究_第5頁(yè)
資源描述:

《安全協(xié)議進(jìn)化生成與模態(tài)邏輯驗(yàn)證研究》由會(huì)員上傳分享,免費(fèi)在線閱讀,更多相關(guān)內(nèi)容在學(xué)術(shù)論文-天天文庫(kù)。

1、中國(guó)科學(xué)技術(shù)大學(xué)博士學(xué)位論文安全協(xié)議進(jìn)化生成與模態(tài)邏輯驗(yàn)證研究姓名:毛晨曉申請(qǐng)學(xué)位級(jí)別:博士專業(yè):計(jì)算機(jī)應(yīng)用指導(dǎo)教師:王煦法20050501摘要中國(guó)科學(xué)技術(shù)人學(xué)博士學(xué)位論文性、認(rèn)證性、不叮否認(rèn)性、保密性、原子性、以及交易規(guī)模和協(xié)議效率方面等性質(zhì)的電子商務(wù)協(xié)}義。(4)深入地研究了基于模態(tài)邏輯的安全協(xié)議形式化驗(yàn)證方法。①提出了用模態(tài)邏輯來(lái)分析安全協(xié)議密碼系統(tǒng)相關(guān)缺陷的方法。其基本思想是擴(kuò)展Dolev.Yao密碼系統(tǒng)模型,不采用完善的密碼系統(tǒng)假設(shè)。具體而言,本論文以CKT5邏輯為基礎(chǔ),以對(duì)稱密碼算法為重點(diǎn),將序列密碼和分組密碼算法的特性以邏輯推理規(guī)則的形式引入到CKT5邏輯框架中,使得擴(kuò)展后的

2、CKT5邏輯能夠用于分析安全協(xié)議密碼系統(tǒng)相關(guān)缺陷。②提出了用模態(tài)邏輯來(lái)分析安全協(xié)議猜測(cè)攻擊的方法。其基本思想是增強(qiáng)Dolev-Yao攻擊者模型,使攻擊者具備密碼分析能力。具體而言,以CKT5邏輯為基礎(chǔ),進(jìn)行了多方面的擴(kuò)展。首先增加了公鑰密碼體制和Vemam加密機(jī)制,增強(qiáng)了其描述協(xié)議的能力。接著在CKT5邏輯中引入了一組規(guī)則使主體具備猜測(cè)和驗(yàn)證口令的能力。然后給出在線猜測(cè)攻擊定理以反映在線猜測(cè)攻擊的特點(diǎn)。并通過(guò)相關(guān)定理的證明,簡(jiǎn)化了猜測(cè)攻擊的分析過(guò)程。擴(kuò)展后的CKT5邏輯能夠用于分析安全協(xié)議的多種猜測(cè)攻擊,且比現(xiàn)有方法更加簡(jiǎn)潔和商效。安全協(xié)議自動(dòng)生成與驗(yàn)證研究是安全協(xié)議研究領(lǐng)域的熱點(diǎn)和難點(diǎn)之

3、一。安全協(xié)議自動(dòng)生成與驗(yàn)證研究,能夠促進(jìn)安全協(xié)議設(shè)計(jì)的自動(dòng)化,以滿足不斷增長(zhǎng)的安全協(xié)議應(yīng)用需求。安全協(xié)議的自動(dòng)生成與驗(yàn)證,不但具有重要的研究?jī)r(jià)值,而且對(duì)于解決安全協(xié)議難于設(shè)計(jì)的問題有著引人注目的現(xiàn)實(shí)意義和廣闊的應(yīng)用前景。ll關(guān)鍵詞:安全協(xié)議:進(jìn)化計(jì)算:形式化驗(yàn)證;模態(tài)邏輯Abstract中國(guó)科學(xué)技術(shù)大學(xué)博士學(xué)位論文AbstractWithcomputernetworksbecomingmoreandmorepopularizedinsocialproductionanddailylife,andalsowiththerapiddevelopmentofnetworkeconomyofwhi

4、che-commerceisatypicalrepresentation,securityprotocolsplaymoreandmoreimportantrolesinthefieldsofIntemet—basedpersonalandcommercialtransactions.Inthesefieldsthereisafastincreasingdemandforsecufityprotocols.However,itisnotoriouslydifficulttodesignandanalyzesecurityprotocols,Thepurposeofthisdissertat

5、ionistoexploreandresearchintoformalandautomatedarialysisanddesignmethodsofsecufityprotocols,Automaticgenerationandverificationofsecurityprotocolsisstudiedfromseveralaspectsincludingmodels,methodsandapplications.Amodelforautomaticgenerationandverificationofsecurityprotocolsisgivenatfirst.Thenametho

6、dforautomaticgenerationandverificationofauthenticationprotocolsispresentedtovalidatethemodel.Thereafter,foltherresearchesintotwokeypointsofthemodeIarecarriedout,includinggenerationapproachesandverificationapproaches.Themainresearchworkofthisdissertationcanbesummarizedasfollows:(1)Amodelforautomati

7、cgenerationandverificationofsecurityprotocolsisgiven,whichisusedtoguidetheresearchofautomaticgenerationandverificationmethodsofsecurityprotocolsTwokeypointsofthemodelarepointedout,i.e.generationapproachesandverif

當(dāng)前文檔最多預(yù)覽五頁(yè),下載文檔查看全文

此文檔下載收益歸作者所有

當(dāng)前文檔最多預(yù)覽五頁(yè),下載文檔查看全文
溫馨提示:
1. 部分包含數(shù)學(xué)公式或PPT動(dòng)畫的文件,查看預(yù)覽時(shí)可能會(huì)顯示錯(cuò)亂或異常,文件下載后無(wú)此問題,請(qǐng)放心下載。
2. 本文檔由用戶上傳,版權(quán)歸屬用戶,天天文庫(kù)負(fù)責(zé)整理代發(fā)布。如果您對(duì)本文檔版權(quán)有爭(zhēng)議請(qǐng)及時(shí)聯(lián)系客服。
3. 下載前請(qǐng)仔細(xì)閱讀文檔內(nèi)容,確認(rèn)文檔內(nèi)容符合您的需求后進(jìn)行下載,若出現(xiàn)內(nèi)容與標(biāo)題不符可向本站投訴處理。
4. 下載文檔時(shí)可能由于網(wǎng)絡(luò)波動(dòng)等原因無(wú)法下載或下載錯(cuò)誤,付費(fèi)完成后未能成功下載的用戶請(qǐng)聯(lián)系客服處理。
关闭