發(fā)布時間：2018-06-22 21:10

  本文選題：反例 + 模型檢測�。� 參考：《電子科技大學學報》2013年05期

【摘要】：提出一種基于模型校驗的策略沖突檢測新方法。首先通過形式化描述語言進行系統(tǒng)建模,采用時態(tài)邏輯表征策略沖突的系統(tǒng)屬性,然后利用NuSMV模型檢測器驗證屬性的可滿足性,并根據模型檢測器產生的反例軌跡追溯策略沖突點。該方法可提高策略沖突檢測的效率。
[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.
【作者單位】： 北京理工大學機電學院;北京理工大學軟件安全工程技術北京市重點實驗室;北京理工大學軟件學院;
【基金】：國家863項目(2009AA01Z433)
【分類號】：TP393.08

【參考文獻】

相關期刊論文 前3條

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

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

3 程亮;張陽;;基于UML和模型檢測的安全模型驗證方法[J];計算機學報;2009年04期

相關博士學位論文 前1條

1 吳蓓;安全策略轉換關鍵技術研究[D];解放軍信息工程大學;2010年

【共引文獻】

相關期刊論文 前10條

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

2 胡媛媛;;利用軟集成設計實時網絡程序框架[J];電子技術;2011年10期

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

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

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

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

7 唐成華;余順爭;;基于特征的網絡安全策略驗證[J];計算機研究與發(fā)展;2009年11期

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

9 倪俊;陳曉蘇;劉輝宇;李勁;;網絡安全策略求精一致性檢測和沖突消解機制的研究[J];計算機科學;2011年02期

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

相關博士學位論文 前7條

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

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

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

4 梅芳;基于策略的移動網絡自主管理機制研究[D];吉林大學;2010年

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

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

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

相關碩士學位論文 前10條

1 韓冰;線性時序邏輯在失業(yè)保險審計中的應用研究[D];哈爾濱工程大學;2010年

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

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

4 呂審;NuSMV模型檢測的研究及應用[D];武漢理工大學;2011年

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

6 李華;智能化通信網絡綜合管理技術[D];電子科技大學;2011年

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

8 晏鴻敏;基于UML和鏡像策略的3G無線網絡鏡像技術研究[D];上海交通大學;2011年

9 呂飛;基于混合式P2P網絡的NAT穿越技術的研究與應用[D];大連理工大學;2011年

10 彭洪德;四川建院學生資助管理系統(tǒng)的設計與實現[D];電子科技大學;2011年

【二級參考文獻】

相關期刊論文 前10條

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

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

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

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

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

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

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

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

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

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

相關博士學位論文 前1條

1 郎風華;基于人工智能理論的網絡安全管理關鍵技術的研究[D];北京郵電大學;2008年

相關碩士學位論文 前4條

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

2 田濤;基于防火墻的企業(yè)網絡安全策略及實現技術研究[D];中國科學院研究生院（計算技術研究所）;2004年

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

4 王永亮;網絡安全設備策略沖突檢測與消解技術研究[D];解放軍信息工程大學;2008年

【相似文獻】

相關期刊論文 前10條

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

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

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

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

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

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

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

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

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

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

相關會議論文 前7條

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

2 肖美華;鄧宸芳;馬小薏;薛錦云;江耘;;網絡安全認證協(xié)議形式化分析[A];第二十次全國計算機安全學術交流會論文集[C];2005年

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

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

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

6 余興超;馬爭先;王玉斌;董榮勝;;基于UPPAAL的簡單網絡支付協(xié)議形式化驗證[A];廣西計算機學會2010年學術年會論文集[C];2010年

7 劉艷芳;丁帥;李建欣;張毅;;一種基于攻擊樹的網絡攻擊路徑生成方法[A];全國第20屆計算機技術與應用學術會議（CACIS·2009）暨全國第1屆安全關鍵技術與應用學術會議論文集（上冊）[C];2009年

相關博士學位論文 前10條

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

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

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

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

5 門鵬;基于Petri網的Web服務組合相關技術研究[D];西安電子科技大學;2009年

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

7 王小兵;面向對象MSVL語言及其在組合Web服務驗證中的應用[D];西安電子科技大學;2009年

8 宋波;Web應用交互的建模和測試用例生成[D];上海大學;2010年

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

10 傅朝陽;面向實時任務求解的自治服務協(xié)同模型、形式語義及其驗證[D];浙江大學;2010年

相關碩士學位論文 前10條

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

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

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

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

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

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

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

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

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

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

，

本文編號：2054236