本文關(guān)鍵詞：基于SPIN的Andrew Secure RPC協(xié)議并行攻擊模型檢測(cè)　出處：《計(jì)算機(jī)科學(xué)》2015年07期 　論文類(lèi)型：期刊論文

  更多相關(guān)文章： Andrew Secure RPC協(xié)議 模型檢測(cè) SPIN 組合身份建模 并行攻擊

【摘要】：Andrew Secure RPC協(xié)議具有身份認(rèn)證和秘鑰交換功能,其因簡(jiǎn)潔明了而被廣泛應(yīng)用于對(duì)稱(chēng)密鑰加密體系中。模型檢測(cè)技術(shù)具有高度自動(dòng)化的優(yōu)點(diǎn),在協(xié)議安全性驗(yàn)證領(lǐng)域得到廣泛應(yīng)用,但模型檢測(cè)方法只能檢測(cè)到一輪協(xié)議會(huì)話中存在的攻擊,難以檢測(cè)到多輪并行會(huì)話中存在的并行攻擊。針對(duì)Andrew Secure RPC協(xié)議運(yùn)行環(huán)境中存在的并行性與可能出現(xiàn)的安全隱患,提出了組合身份建模方法。該方法運(yùn)用著名的SPIN模型檢測(cè)工具,對(duì)Andrew Secure RPC協(xié)議進(jìn)行模型檢測(cè),從而得到攻擊序列圖,成功發(fā)現(xiàn)并行反射攻擊和類(lèi)缺陷攻擊。上述組合身份建模方法為復(fù)雜環(huán)境下協(xié)議的模型檢測(cè)提供了新的方向。
【作者單位】： 華東交通大學(xué)軟件學(xué)院;
【分類(lèi)號(hào)】：TP393.08
【正文快照】： 到稿日期:2014-06-25返修日期:2014-09-14本文受?chē)?guó)家自然科學(xué)基金(61163005),計(jì)算機(jī)軟件新技術(shù)國(guó)家重點(diǎn)實(shí)驗(yàn)室開(kāi)放課題(KFKT2012B18),江西省高�？萍悸涞赜�(jì)劃項(xiàng)目(KJLD13038),江西省自然科學(xué)基金(2010GZS0150,20132BAB201033)資助。安全協(xié)議是以密碼學(xué)為基礎(chǔ)的消息交換協(xié)議,其

【相似文獻(xiàn)】

中國(guó)重要會(huì)議論文全文數(shù)據(jù)庫(kù) 前7條

1 高靜;曹子寧;;基于空間邏輯和計(jì)算樹(shù)邏輯的模型檢測(cè)[A];2009年中國(guó)高校通信類(lèi)院系學(xué)術(shù)研討會(huì)論文集[C];2009年

2 許梅;曹子寧;;基于謂詞μ演算和空間邏輯的模型檢測(cè)算法研究[A];2009年中國(guó)高校通信類(lèi)院系學(xué)術(shù)研討會(huì)論文集[C];2009年

3 何青;駱翔宇;蘇開(kāi)樂(lè);;對(duì)弈必勝策略的符號(hào)化模型檢測(cè)[A];2006年全國(guó)理論計(jì)算機(jī)科學(xué)學(xué)術(shù)年會(huì)論文集[C];2006年

4 王飛明;胡元闖;董榮勝;;模型檢測(cè)中狀態(tài)爆炸及其優(yōu)化策略研究[A];廣西計(jì)算機(jī)學(xué)會(huì)2008年年會(huì)論文集[C];2008年

5 陳道喜;張廣泉;陳冬火;;NSPK協(xié)議的Spin模型檢測(cè)[A];2008年全國(guó)開(kāi)放式分布與并行計(jì)算機(jī)學(xué)術(shù)會(huì)議論文集(下冊(cè))[C];2008年

6 邢立國(guó);張光甫;劉薇;胥維昌;金一和;;人皮膚模型評(píng)價(jià)殺菌類(lèi)農(nóng)藥腐蝕/刺激性研究[A];2014線粒體毒性與基于毒性通路的安全性評(píng)價(jià)新策略學(xué)術(shù)研討會(huì)暨中國(guó)毒理學(xué)會(huì)毒理學(xué)替代法與轉(zhuǎn)化毒理學(xué)專(zhuān)業(yè)委員會(huì)成立大會(huì)論文集[C];2014年

7 張明玉;;我國(guó)對(duì)外開(kāi)放、通貨膨脹與經(jīng)濟(jì)增長(zhǎng)相關(guān)關(guān)系的模型檢測(cè)[A];面向21世紀(jì)的科技進(jìn)步與社會(huì)經(jīng)濟(jì)發(fā)展（下冊(cè)）[C];1999年

中國(guó)博士學(xué)位論文全文數(shù)據(jù)庫(kù) 前10條

1 江華;界程演算模型檢測(cè)[D];貴州大學(xué);2008年

2 林榮德;移動(dòng)界程演算及模型檢測(cè)應(yīng)用的關(guān)鍵問(wèn)題研究[D];華南理工大學(xué);2010年

3 劉劍;傳值進(jìn)程與移動(dòng)進(jìn)程的模型檢測(cè)方法[D];中國(guó)科學(xué)院研究生院（軟件研究所）;2005年

4 劉志鋒;模型檢測(cè)中關(guān)鍵技術(shù)的研究及其應(yīng)用[D];南京大學(xué);2011年

5 朱維軍;時(shí)間區(qū)間時(shí)序邏輯模型檢測(cè)：理論、算法及應(yīng)用[D];西安電子科技大學(xué);2011年

6 陳冬火;超協(xié)調(diào)時(shí)序邏輯及其模型檢測(cè)方法[D];中國(guó)科學(xué)院研究生院（成都計(jì)算機(jī)應(yīng)用研究所）;2006年

7 田聰;命題投影時(shí)序邏輯的判定性、復(fù)雜性、表達(dá)性及模型檢測(cè)[D];西安電子科技大學(xué);2010年

8 黃宏濤;基于懶惰切片的模型檢測(cè)技術(shù)研究[D];哈爾濱工程大學(xué);2012年

9 劉金卓;基于符號(hào)化模型檢測(cè)的軟件演化過(guò)程模型驗(yàn)證[D];云南大學(xué);2013年

10 吳駿;多Agent聯(lián)盟規(guī)范系統(tǒng)研究[D];南京大學(xué);2011年

中國(guó)碩士學(xué)位論文全文數(shù)據(jù)庫(kù) 前10條

1 張衍志;符號(hào)化模型檢測(cè)算法的研究[D];吉林大學(xué);2009年

2 黎吾平;模型檢測(cè)在軟件方面的應(yīng)用[D];吉林大學(xué);2008年

3 吳小娟;并行完備模型檢測(cè)技術(shù)的研究[D];電子科技大學(xué);2013年

4 姜志敏;模型檢測(cè)在配置中的應(yīng)用[D];吉林大學(xué);2010年

5 金怡愛(ài);基于模型檢測(cè)方法的規(guī)劃[D];吉林大學(xué);2005年

6 施小純;基于反例搜索的啟發(fā)式模型檢測(cè)算法的研究[D];中國(guó)科學(xué)院研究生院（軟件研究所）;2004年

7 陳亞軍;模型檢測(cè)在安全協(xié)議形式化驗(yàn)證中的應(yīng)用[D];電子科技大學(xué);2012年

8 殷朝冉;測(cè)試目的引導(dǎo)的模型檢測(cè)方法與技術(shù)研究[D];北方工業(yè)大學(xué);2015年

9 高靜;面向環(huán)境演算系統(tǒng)的模型檢測(cè)算法的研究[D];南京航空航天大學(xué);2009年

10 廉智超;模型檢測(cè)在模型診斷領(lǐng)域中的應(yīng)用[D];吉林大學(xué);2007年

，

本文編號(hào)：1310502