本文選題：反例 + 模型檢測��； 參考：《電子科技大學(xué)學(xué)報(bào)》2013年05期

【摘要】：提出一種基于模型校驗(yàn)的策略沖突檢測新方法。首先通過形式化描述語言進(jìn)行系統(tǒng)建模,采用時(shí)態(tài)邏輯表征策略沖突的系統(tǒng)屬性,然后利用NuSMV模型檢測器驗(yàn)證屬性的可滿足性,并根據(jù)模型檢測器產(chǎn)生的反例軌跡追溯策略沖突點(diǎn)。該方法可提高策略沖突檢測的效率。
[Abstract]:A new strategy conflict detection method based on model checking is proposed. Firstly, the system is modeled by formal description language, and the system attributes of policy conflict are represented by temporal logic. Then, NuSMV model detector is used to verify the satisfiability of attributes. According to the counter-example trajectory generated by the model detector, the conflict point of the strategy is traced back. This method can improve the efficiency of policy conflict detection.
【作者單位】： 北京理工大學(xué)機(jī)電學(xué)院;北京理工大學(xué)軟件安全工程技術(shù)北京市重點(diǎn)實(shí)驗(yàn)室;北京理工大學(xué)軟件學(xué)院;
【基金】：國家863項(xiàng)目(2009AA01Z433)
【分類號】：TP393.08

【參考文獻(xiàn)】

相關(guān)期刊論文 前3條

1 姚鍵 ,茅兵 ,謝立;一種基于有向圖模型的安全策略沖突檢測方法[J];計(jì)算機(jī)研究與發(fā)展;2005年07期

2 李祥軍;孟洛明;焦利;;網(wǎng)管系統(tǒng)策略沖突解決的結(jié)果中存在的問題及檢測與解決方法[J];計(jì)算機(jī)研究與發(fā)展;2006年07期

3 程亮;張陽;;基于UML和模型檢測的安全模型驗(yàn)證方法[J];計(jì)算機(jī)學(xué)報(bào);2009年04期

相關(guān)博士學(xué)位論文 前1條

1 吳蓓;安全策略轉(zhuǎn)換關(guān)鍵技術(shù)研究[D];解放軍信息工程大學(xué);2010年

【共引文獻(xiàn)】

相關(guān)期刊論文 前10條

1 張屹;魏學(xué)業(yè);何春明;;基于時(shí)間化UML的安全通信模型檢測[J];電子測量與儀器學(xué)報(bào);2010年10期

2 胡媛媛;;利用軟集成設(shè)計(jì)實(shí)時(shí)網(wǎng)絡(luò)程序框架[J];電子技術(shù);2011年10期

3 李鳳華;蘇斢;史國振;馬建峰;;訪問控制模型研究進(jìn)展及發(fā)展趨勢[J];電子學(xué)報(bào);2012年04期

4 謝琳;;Geopriv協(xié)議形式化分析與模型檢測[J];計(jì)算機(jī)光盤軟件與應(yīng)用;2013年17期

5 任占陽;望育梅;張琳;;一種新的策略沖突解決方法的研究[J];信息通信;2010年01期

6 張濤;黃少濱;黃宏濤;呂天陽;劉剛;;一種UML狀態(tài)圖模型檢測方法[J];哈爾濱工程大學(xué)學(xué)報(bào);2011年08期

7 唐成華;余順爭;;基于特征的網(wǎng)絡(luò)安全策略驗(yàn)證[J];計(jì)算機(jī)研究與發(fā)展;2009年11期

8 梅芳;劉衍珩;張旭利;古天野;王旺;;移動網(wǎng)絡(luò)資源管理策略的動態(tài)沖突消解機(jī)制[J];吉林大學(xué)學(xué)報(bào)(工學(xué)版);2009年02期

9 倪俊;陳曉蘇;劉輝宇;李勁;;網(wǎng)絡(luò)安全策略求精一致性檢測和沖突消解機(jī)制的研究[J];計(jì)算機(jī)科學(xué);2011年02期

10 翟浩良;韓道軍;李磊;;基于邏輯和辯論的安全策略一致性研究[J];計(jì)算機(jī)科學(xué)與探索;2012年04期

相關(guān)博士學(xué)位論文 前7條

1 焦素云;基于概念格的動態(tài)策略存取模型[D];吉林大學(xué);2011年

2 張立勇;軟件源代碼安全分析研究[D];西安電子科技大學(xué);2011年

3 皮建勇;分布式并行系統(tǒng)若干安全技術(shù)的研究[D];電子科技大學(xué);2008年

4 梅芳;基于策略的移動網(wǎng)絡(luò)自主管理機(jī)制研究[D];吉林大學(xué);2010年

5 趙也非;動態(tài)UML子圖的形式語義研究[D];華東師范大學(xué);2010年

6 張濤;復(fù)雜信息系統(tǒng)模型的形式化驗(yàn)證方法研究[D];哈爾濱工程大學(xué);2012年

7 李赤松;訪問控制中授權(quán)一致性問題的研究[D];華中科技大學(xué);2012年

相關(guān)碩士學(xué)位論文 前10條

1 韓冰;線性時(shí)序邏輯在失業(yè)保險(xiǎn)審計(jì)中的應(yīng)用研究[D];哈爾濱工程大學(xué);2010年

2 朱耀強(qiáng);網(wǎng)格安全策略沖突檢測及其消解機(jī)制的研究[D];長春工業(yè)大學(xué);2010年

3 潘國棟;基于CORBA的信息系統(tǒng)安全組件管理研究[D];西安電子科技大學(xué);2009年

4 呂審;NuSMV模型檢測的研究及應(yīng)用[D];武漢理工大學(xué);2011年

5 陳倩倩;基于實(shí)時(shí)UML對實(shí)時(shí)系統(tǒng)LTE無線通信系統(tǒng)信令子系統(tǒng)（RRC系統(tǒng)）建模[D];華東師范大學(xué);2011年

6 李華;智能化通信網(wǎng)絡(luò)綜合管理技術(shù)[D];電子科技大學(xué);2011年

7 李添翼;多策略支持下的策略沖突檢測與消解研究[D];華中科技大學(xué);2011年

8 晏鴻敏;基于UML和鏡像策略的3G無線網(wǎng)絡(luò)鏡像技術(shù)研究[D];上海交通大學(xué);2011年

9 呂飛;基于混合式P2P網(wǎng)絡(luò)的NAT穿越技術(shù)的研究與應(yīng)用[D];大連理工大學(xué);2011年

10 彭洪德;四川建院學(xué)生資助管理系統(tǒng)的設(shè)計(jì)與實(shí)現(xiàn)[D];電子科技大學(xué);2011年

【二級參考文獻(xiàn)】

相關(guān)期刊論文 前10條

1 何再朗,田敬東,張毓森;策略沖突類型的細(xì)化及檢測方法的改進(jìn)[J];吉林大學(xué)學(xué)報(bào)(信息科學(xué)版);2005年03期

2 李莉,任秀麗,欒貴興;基于策略的分布式網(wǎng)絡(luò)管理系統(tǒng)[J];東北大學(xué)學(xué)報(bào);2002年06期

3 易漢文;由合理路徑阻抗推求區(qū)間出行阻抗[J];系統(tǒng)工程;1995年04期

4 何再朗,田敬東,張毓森;策略沖突分析、檢測及解決方案[J];蘭州理工大學(xué)學(xué)報(bào);2005年05期

5 王震;袁兆山;;基于本體的數(shù)據(jù)集成沖突消解[J];合肥工業(yè)大學(xué)學(xué)報(bào)(自然科學(xué)版);2010年03期

6 陳冬松,潘成勝,俞承志,王光興;一種基于策略的配置管理思想[J];火力與指揮控制;2003年05期

7 夏春和;魏玉娣;李肖堅(jiān);王海泉;何巍;;計(jì)算機(jī)網(wǎng)絡(luò)防御策略描述語言研究[J];計(jì)算機(jī)研究與發(fā)展;2009年01期

8 梅芳;劉衍珩;張旭利;古天野;王旺;;移動網(wǎng)絡(luò)資源管理策略的動態(tài)沖突消解機(jī)制[J];吉林大學(xué)學(xué)報(bào)(工學(xué)版);2009年02期

9 李祥軍,邱雪松,孟洛明;基于策略的網(wǎng)管中策略條件“或”運(yùn)算的問題及解決方法[J];計(jì)算機(jī)工程與應(yīng)用;2005年12期

10 黃俊;韓玲莉;;IPSec策略沖突發(fā)現(xiàn)形式化技術(shù)的研究[J];計(jì)算機(jī)工程與應(yīng)用;2007年06期

相關(guān)博士學(xué)位論文 前1條

1 郎風(fēng)華;基于人工智能理論的網(wǎng)絡(luò)安全管理關(guān)鍵技術(shù)的研究[D];北京郵電大學(xué);2008年

相關(guān)碩士學(xué)位論文 前4條

1 亢崳;基于多層策略網(wǎng)絡(luò)管理系統(tǒng)研究[D];中南大學(xué);2005年

2 田濤;基于防火墻的企業(yè)網(wǎng)絡(luò)安全策略及實(shí)現(xiàn)技術(shù)研究[D];中國科學(xué)院研究生院（計(jì)算技術(shù)研究所）;2004年

3 王柏昀;面向多主體的政策描述規(guī)范及沖突研究[D];湖南大學(xué);2009年

4 王永亮;網(wǎng)絡(luò)安全設(shè)備策略沖突檢測與消解技術(shù)研究[D];解放軍信息工程大學(xué);2008年

【相似文獻(xiàn)】

相關(guān)期刊論文 前10條

1 李衛(wèi)民;徐炳雪;;基于NuSMV的攻擊圖模型生成技術(shù)研究[J];硅谷;2010年19期

2 周立青;楊晉吉;;樂觀合同簽訂協(xié)議的模型檢測分析[J];計(jì)算機(jī)工程;2011年07期

3 高昀;;信息系統(tǒng)的可生存性建模與分析研究[J];甘肅科技;2010年21期

4 林璇;;模型檢測方法在入侵檢測中的應(yīng)用研究[J];現(xiàn)代計(jì)算機(jī)(專業(yè)版);2009年02期

5 徐有福;文偉平;萬正蘇;;基于漏洞模型檢測的安全漏洞挖掘方法研究[J];信息網(wǎng)絡(luò)安全;2011年08期

6 吉猛;胡克瑾;;基于模型檢測的電子商務(wù)鑒證技術(shù)[J];陜西師范大學(xué)學(xué)報(bào)(自然科學(xué)版);2006年04期

7 李忠慧;張廣泉;;基于UPPAAL的NS密碼協(xié)議模型檢測分析[J];重慶師范大學(xué)學(xué)報(bào)(自然科學(xué)版);2009年04期

8 楊晉吉,蘇開樂;電子商務(wù)中安全協(xié)議的驗(yàn)證方法[J];計(jì)算機(jī)工程與應(yīng)用;2003年19期

9 劉芳;魏昭;董榮勝;;基于SPIN的SAS協(xié)議和NS公鑰協(xié)議分析[J];廣西科學(xué)院學(xué)報(bào);2008年04期

10 陳妍;唐成華;吳丹;;基于模型檢測的工作流訪問控制策略驗(yàn)證[J];計(jì)算機(jī)應(yīng)用研究;2010年02期

相關(guān)會議論文 前7條

1 劉芳;魏昭;董榮勝;;基于SPIN的協(xié)議分析技術(shù)研究[A];廣西計(jì)算機(jī)學(xué)會2008年年會論文集[C];2008年

2 肖美華;鄧宸芳;馬小薏;薛錦云;江耘;;網(wǎng)絡(luò)安全認(rèn)證協(xié)議形式化分析[A];第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會論文集[C];2005年

3 孫守卿;李廉;章超;李彩虹;;基于模型檢測工具SPIN的安全協(xié)議形式化分析[A];2005年全國理論計(jì)算機(jī)科學(xué)學(xué)術(shù)年會論文集[C];2005年

4 謝鴻波;周明天;;安全協(xié)議的形式化技術(shù):述評[A];’2004計(jì)算機(jī)應(yīng)用技術(shù)交流會議論文集[C];2004年

5 奚琪;王清賢;曾勇軍;;惡意代碼檢測技術(shù)綜述[A];計(jì)算機(jī)研究新進(jìn)展（2010）——河南省計(jì)算機(jī)學(xué)會2010年學(xué)術(shù)年會論文集[C];2010年

6 余興超;馬爭先;王玉斌;董榮勝;;基于UPPAAL的簡單網(wǎng)絡(luò)支付協(xié)議形式化驗(yàn)證[A];廣西計(jì)算機(jī)學(xué)會2010年學(xué)術(shù)年會論文集[C];2010年

7 劉艷芳;丁帥;李建欣;張毅;;一種基于攻擊樹的網(wǎng)絡(luò)攻擊路徑生成方法[A];全國第20屆計(jì)算機(jī)技術(shù)與應(yīng)用學(xué)術(shù)會議（CACIS·2009）暨全國第1屆安全關(guān)鍵技術(shù)與應(yīng)用學(xué)術(shù)會議論文集（上冊）[C];2009年

相關(guān)博士學(xué)位論文 前10條

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

2 張玉清;計(jì)算機(jī)通信網(wǎng)安全協(xié)議的分析研究[D];西安電子科技大學(xué);2000年

3 文靜華;電子商務(wù)協(xié)議形式化方法及模型檢測技術(shù)的研究與應(yīng)用[D];貴州大學(xué);2006年

4 陳靖;帶實(shí)時(shí)的傳值與移動系統(tǒng)研究[D];中國科學(xué)院研究生院（軟件研究所）;2003年

5 門鵬;基于Petri網(wǎng)的Web服務(wù)組合相關(guān)技術(shù)研究[D];西安電子科技大學(xué);2009年

6 范紅;安全協(xié)議形式化分析理論與方法[D];中國人民解放軍信息工程大學(xué);2003年

7 王小兵;面向?qū)ο驧SVL語言及其在組合Web服務(wù)驗(yàn)證中的應(yīng)用[D];西安電子科技大學(xué);2009年

8 宋波;Web應(yīng)用交互的建模和測試用例生成[D];上海大學(xué);2010年

9 龍士工;串空間理論及其在安全協(xié)議分析中的應(yīng)用研究[D];貴州大學(xué);2007年

10 傅朝陽;面向?qū)崟r(shí)任務(wù)求解的自治服務(wù)協(xié)同模型、形式語義及其驗(yàn)證[D];浙江大學(xué);2010年

相關(guān)碩士學(xué)位論文 前10條

1 袁建廷;鑒別協(xié)議的分析研究[D];西安電子科技大學(xué);2008年

2 高丹丹;無線認(rèn)證協(xié)議的模型檢測與分析研究[D];長春理工大學(xué);2010年

3 劉學(xué)鋒;安全協(xié)議形式化分析及其應(yīng)用[D];湘潭大學(xué);2004年

4 吳建耀;電子商務(wù)安全協(xié)議的形式化分析技術(shù)研究[D];西安電子科技大學(xué);2005年

5 吳瑞龍;一種基于有色Petri網(wǎng)模型的安全協(xié)議檢測技術(shù)的研究[D];廣西大學(xué);2005年

6 鄧保華;動態(tài)Web服務(wù)組合中業(yè)務(wù)流程建模環(huán)境的研究與實(shí)現(xiàn)[D];國防科學(xué)技術(shù)大學(xué);2005年

7 劉秀英;計(jì)算機(jī)通信網(wǎng)安全協(xié)議形式化分析研究[D];西安電子科技大學(xué);2004年

8 黃瑛;SET協(xié)議支付過程分析及模型檢測[D];貴州大學(xué);2006年

9 阮小黎;基于模型檢測的C語言安全信息流研究[D];清華大學(xué);2007年

10 黨繼勝;基于SVO邏輯的電子商務(wù)協(xié)議形式化分析與研究[D];貴州大學(xué);2007年

，

本文編號：2054236