導航：安全管理網>> 安全論文>> 綜合安全論文>>正文

互斥協議的安全性分析

文檔作者：趙夢龍１唐鄭熠２萬良3 韋立４文檔來源：１．貴州職業技術學院信息技術系２．福建工程學院 3．貴州大學計算機科學與技術學院４．貴州師范大學數學與計算機科學學院		點擊數：	更新時間： 2022年04月11日
下載地址：點擊這里	文件大小： 812.40 KB 共3頁	文檔格式： PDF	下載點數： 1 點（VIP免費）

全屏查看

內容預覽 [文件共3頁]

本文件共3頁，如需編輯使用，請下載。

注：預覽效果可能會出現部分文字亂碼（如口口口）、內容顯示不全等問題，下載是正常的。

	文件大小：812.40 KB 共3頁文件格式：PDF 下載點數：1 點（VIP會員免費）

下一篇：基于LEACH協議的安全節能路由算法研究

上一篇：基于匹配策略的安全協議重構分析

文本預覽

僅提取頁面文字內容，供快速閱讀使用。

收稿日期： ２0１４-0４-１１; 修回日期： ２0１４-06-09　　基金項目： 國家自然科學基金資助項目(6１30900);貴州省自然科學基金資助項目( Ｊ
［２0１１］２3２８);福建工程學院科研啟動基金資助項目(GＹ-Ｚ１3１１２)
作者簡介：趙夢龍(１9８１-),男(通信作者),河南駐馬店人,講師,碩士,主要研究方向為形式化方法、信息安全等( ｈａppｙboｙｚ＿ｈａo@１２6．coｍ);
唐鄭熠(１9８４-),男,福建福州人,講師,博士,主要研究方向為形式化方法、服務計算;萬良(１9７４-),男,貴州貴陽人,副教授,博士(后),主要研究方
向為形式化方法、信息安全;韋立(１9８１-),男,廣西都安人,副教授,博士,主要研究方向為可計算性與計算復雜性．
互斥協議的安全性分析*
趙夢龍１, 唐鄭熠２, 萬　良3, 韋　立４
(１．貴州職業技術學院信息技術系, 貴陽5500２3; ２．福建工程學院信息科學與工程學院, 福州350１１８; 3．貴
州大學計算機科學與技術學院, 貴陽5500２3; ４．貴州師范大學數學與計算機科學學院, 貴陽55000４)
摘　要： 安全性和活性是兩大基本的系統屬性,對于指導系統的設計與驗證具有重要意義。通過對它們原始定
義的形式化梳理,發現其缺乏對狀態序列的具體約束。針對這一問題,使用對系統動作刻畫更完善的行為時序
邏輯進行了重定義,加入了初始狀態和轉移條件的約束。以此為基礎,對互斥這一并發系統的典型屬性進行了
形式化的分析,由此說明如何判斷一個屬性是否滿足安全性或活性的定義。該技術為實現系統性質的自動推理
與驗證提供了形式化基礎。
關鍵詞： 互斥協議; 屬性分類; 安全性; 活性; 行為時序邏輯
中圖分類號： ＴＰ309．１　　　文獻標志碼： Ａ　　　　　文章編號： １00１-3695(２0１5)05-１４８6-03
ｄoｉ：１0．3969/j．ｉｓｓｎ．１00１-3695．２0１5．05．05２
Sａｆｅｔｙ ａｎａｌｙｓｉｓ oｆ ｍｕｔｕａｌ ｅｘcｌｕｓｉoｎ pｒoｔocoｌ
ＺＨＡO Ｍｅｎg-ｌoｎg１, ＴＡＮG Ｚｈｅｎg-ｙｉ２ , ＷＡＮ Ｌｉａｎg3 , ＷＥＩ Ｌｉ４
(１.Ｄｅｐｔ.ｏfＩｎfｏrｍａｔｉｏｎ Ｔｅｃｈｎｏｌｏgy, Gｕｉｚｈｏｕ Ｖｏｃａｔｉｏｎａｌ Ｔｅｃｈｎｏｌｏgy Ｉｎsｔｉｔｕｔｅ, Gｕｉyａｎg 5500２3, Ｃｈｉｎａ; ２.Ｓｃｈｏｏｌ ｏfＩｎfｏrｍａｔｉｏｎ Ｓｃｉｅｎｃｅ ＆
Ｅｎgｉｎｅｅrｉｎg, Ｆｕｊｉａｎ Ｕｎｉvｅrsｉｔy ｏfＴｅｃｈｎｏｌｏgy, Ｆｕｚｈｏｕ 350１１８, Ｃｈｉｎａ; 3.Ｓｃｈｏｏｌ ｏfＣｏｍｐｕｔｅr Ｓｃｉｅｎｃｅ ＆Ｔｅｃｈｎｏｌｏgy, Gｕｉｚｈｏｕ Ｕｎｉvｅrsｉｔy, Gｕｉyａｎg
5500２3, Ｃｈｉｎａ; ４.Ｓｃｈｏｏｌ ｏfＭａｔｈｅｍａｔｉｃs ＆Ｃｏｍｐｕｔｅr Ｓｃｉｅｎｃｅ, Gｕｉｚｈｏｕ Ｎｏrｍａｌ Ｕｎｉvｅrsｉｔy, Gｕｉyａｎg 55000４, Ｃｈｉｎａ)
Ａｂsｔｒａｃｔ: Sａｆｅｔｙ ａｎｄ ｌｉｖｅｎｅｓｓ ａｒｅ ｔoｗ bａｓｉc ｔｙpｅｓ oｆ ｓｙｓｔｅｍ pｒopｅｒｔｙ ａｎｄ ａｒｅ ｖｅｒｙ ｕｓｅｆｕｌ ｆoｒ ｔｈｅ ｄｅｓｉgｎ ａｎｄ ｖｅｒｉｆｉcａｔｉoｎ oｆ ｓｙｓｔｅｍ．
Ｔｈｉｓ pａpｅｒ poｉｎｔｅｄ oｕｔ ｔｈｅ ｄｉｓａｄｖａｎｔａgｅ oｆ ｌａcｋｉｎg ｒｅｓｔｒｉcｔｓ ｔo ｓｔａｔｅ ｓｅｑｕｅｎcｅ ｉｎ ｔｈｅｉｒ oｒｉgｉｎａｌ ｄｅｆｉｎｉｔｉoｎ．Ｆoｒ ｔｈｉｓ pｒobｌｅｍ,
ｉｔ gａｖｅ ｒｅｄｅｆｉｎｉｔｉoｎ bｙ ｔｈｅ ｔｅｍpoｒａｌ ｌogｉc oｆ ａcｔｉoｎ ｗｈｉcｈ ｗａｓ ｍoｒｅ ｓｕｉｔａbｌｅ ｔo ｄｅｓcｒｉbｅ ｓｙｓｔｅｍ ａcｔｉoｎ．Ｔｈｅ ｎｅｗ ｆoｒｍａｌ ｄｅｆｉｎｉｔｉoｎ
ａｄｄｅｄ ｉｎｉｔｉａｌ ｓｔａｔｅ ａｎｄ coｎｓｔｒａｉｎｔ coｎｄｉｔｉoｎｓ ｆoｒ ｔｒａｎｓｆｅｒ．Oｎ ｔｈｉｓ bａｓｉｓ, ｉｔ ａｎａｌｙｚｅｄ ｔｈｅ ｍｕｔｕａｌ ｅｘcｌｕｓｉoｎ ｗｈｉcｈ ｗａｓ ｔｈｅ
ｔｙpｉcａｌ pｒopｅｒｔｙ oｆ coｎcｕｒｒｅｎｔ ｓｙｓｔｅｍ bｙ ｆoｒｍａｌ ｍｅｔｈoｄ．Ｉｔ ａｌｓo ｓｈoｗｓ ｔｈａｔ ｈoｗ ｔo jｕｄgｅ ｗｈｅｔｈｅｒ ａ pｒopｅｒｔｙ ｍｅｅｔｓ ｔｈｅ ｄｅｆｉｎｉｔｉoｎ
oｆ ｓａｆｅｔｙ oｒ ｌｉｖｅｎｅｓｓ．Ｔｈｉｓ ｔｅcｈｎoｌogｙ pｒoｖｉｄｅｄ ｔｈｅ ｆoｒｍａｌ bａｓｉc ｆoｒ ｔｈｅ ａｕｔoｍａｔｉc ｒｅａｓoｎｉｎg ａｎｄ ｖｅｒｉｆｉcａｔｉoｎ oｆ ｓｙｓｔｅｍ pｒopｅｒｔｙ．
Ｋｅy ｗｏｒｄs: ｍｕｔｕａｌ ｅｘcｌｕｓｉoｎ pｒoｔocoｌ; cｌａｓｓｉｆｉcａｔｉoｎ oｆ pｒopｅｒｔｉｅｓ; ｓａｆｅｔｙ; ｌｉｖｅｎｅｓｓ; ｔｅｍpoｒａｌ ｌogｉc oｆ ａcｔｉoｎ
O　引言
在操作系統中,為了保證程序最終執行結果的正確性,必
須對并發執行的各進程進行制約,以控制它們的執行速度和對
資源的競爭［１］ 。進程之間的間接制約在操作系統中通常叫互
斥,互斥是系統設計的關鍵問題之一［２］ ,它保證了相互沖突的
并發進程可以共享資源。本文介紹了安全性與活性的形式化
定義,并針對其對狀態序列沒有作具體約束的不足,在行為時
序邏輯中對其進行了重定義。根據安全性和活性的形式化定
義,對互斥協議的安全性進行了形式化的分析,證明了互斥協
議是安全性而不是活性。
1　安全性與活性介紹
１9７７ 年,美國科學家Ｌａｍpoｒｔ 在驗證多線程程序正確性的
過程中,最早提出了將系統的性質分為安全性和活性兩類,并
給出了它們的非形式化定義:
ａ)安全性:規定一些行為不會在系統中發生。
b)活性:規定一些行為必須在系統中發生。
2　安全性與活性的形式化定義
在１9８４ 年,Ｌａｍpoｒｔ 第一次對安全性進行了形式化的定
義,隨后Ａｌpｅｒｎ 和Scｈｎｅｉｄｅｒ 又進一步給出了活性的形式化定
義。Ｌａｍpoｒｔ ［3］ 是行為時序邏輯( ｔｅｍpoｒａｌ ｌogｉc oｆ ａcｔｉoｎ) 的創
立者,而安全性和活性的定義主要也是由他提出或啟發的,其
中的很多概念都被他加入到后來的行為時序邏輯當中。這使
得安全性和活性能夠方便地使用行為時序邏輯進行定義。因
此下面首先介紹安全性和活性的原始定義,然后再以行為時序
邏輯對它們進行更精確的定義。
2．1　原始定義
系統的一次運行用系統狀態的無限序列來表示:
$1 s0 s１ s２
狀態之間的轉移是由于系統執行了某個行為而發生的。
第3２ 卷第5 期
２0１5 年5 月　
計算機應用研究
Ａppｌｉcａｔｉoｎ Ｒｅｓｅａｒcｈ oｆ Coｍpｕｔｅｒｓ
Ｖoｌ．3２ Ｎo．5
Ｍａｙ ２0１5
對于一次不可終止的運行,狀態序列顯然是無限的;而對于一
次可終止的運行,可以通過不斷地重復序列中的最后一個狀態
使其成為無限序列［４］ 。
同時,$［ｉ］ 1 sｉ,$［..ｉ］ 1 s0 s１ s２ sｉ －１ ,$［ ｉ..］ 1 sｉ sｉ ＋１
sｉ ＋２ 。對于兩個運轉α1 s0 s１ s２ sｉ －１ , β 1 sｉ ＋１ sｉ ＋２ sｉ ＋3 ,
αβ1 s0 s１ s２ sｉ －１ sｉ ＋１ sｉ ＋２ sｉ ＋3 。
一個屬性被看做是運轉的集合,其中所包含的元素是滿足
該屬性的運轉［5］ 。如果說系統滿足一個屬性,那么該系統所
有可能的運轉都包含在屬性所描述的集合中。
定義１　屬性(pｒopｅｒｔｙ) ［6］ 。一個屬性Ｐ 被看做是所有符
合滿足該屬性的運轉的集合,一個運轉滿足Ｐ 等價于該運轉
屬于Ｐ 所表示的集合,即α(Ｐ$｜＝Ｐ。
用Ｓ 表示所有系統狀態的集合;用Ｓ*表示所有系統狀態
有限序列的集合,系統狀態的有限序列用來表示系統一次運行
中的部分時刻;用Ｓw 表示所有系統狀態無限序列的集合,系統
狀態的無限序列用來表示系統一次運行。對于有限運轉$(
Ｓ*,｜$｜表示它的長度。
安全性的定義是一些“ 壞的事情” 不會發生,因此如果屬
性Ｐ 是一個安全性,那么當一個運轉不滿足屬性Ｐ 的約束時,
那么在運轉中的某些點上發生了“壞的事情”。“ 壞的事情” 一
旦發生就不可補救,因為安全性要求的是“ 壞的事情” 永遠都
不會發生。
定義２　安全性( ｓａｆｅｔｙ) ［5］ 。屬性Ｐ 是一個安全性,當且
僅當($:$(Ｓw:$｜≠Ｐ  (ｉ: ｉ≥0: (β: β(Ｓw: $［..
ｉ］β｜≠Ｐ)))。
安全性的含義是:安全性Ｐ 中的所有運轉的任意前綴都
可以被擴展為一個或多個屬于Ｐ 的無限運轉。這個定義并沒
有對“壞的事情” 作出具體限制,但它一定是一個獨立的原子
行為,因為一旦一個運轉中出現了“壞的事情”,那么一定是在
一個可確認的點發生的。
活性的定義是在系統運行的過程中,“ 好的事情” 最終會
發生。活性要求系統運行到任何時刻都存在著發生“ 好的事
情”的可能,無論過去“ 好的事情” 是否發生,至少要存在未來
發生的可能。
定義3　活性( ｌｉｖｅｎｅｓｓ) ［5］ 。屬性Ｐ 是一個活性,當且僅
當(α: α(Ｓ*: (β: β(Ｓw: αβ｜＝Ｐ))。
活性的含義是:系統中的任意有限狀態序列都可以被擴展
為一個或多個屬于Ｐ 的無限序列。這個定義同樣沒有對“ 好
的事情”作出具體的規定,甚至沒有限制它必須是一個獨立的
原子行為。但只要求“好的事情”最終會發生,但不是一直( ａｌｗａｙｓ)
發生。
2．2　基于行為時序邏輯的形式化定義
在安全性與活性的原始定義中,對于無限序列集合Ｓw 和
有限序列集合Ｓ*并沒有作出具體的約束。然而一個系統的運
行并不是隨意,系統的初始狀態和狀態之間的轉移是存在著限
制的［6］ 。因此, 本文在行為時序邏輯中對其進行更嚴格的
定義。
下面首先簡要介紹一些ＴＬＡ 中的定義［７ ～9］ 。
定義４　行為( ａcｔｉoｎ)。由變量、原本變量及常量符號組
成的布爾表達式。變量與當前狀態相關,原本變量與下一狀態
相關。
定義5　啞步(ｓｔｕｔｔｅｒｉｎg ｓｔｅpｓ)。啞步是一種特殊的行為,
在該行為發生后,系統中所有變量的值都保持不變。
定義6　標記轉移系統:一個標記轉移系統T＝(Ｓ, Ｉ, ,
%),其中:
ａ)系統中的所有變量的一次有效賦值稱為一個狀態s,所
有的狀態(即所有可能的賦值)構成狀態集合,記為Ｓ。
b)初始狀態ＩＳ。
c) 是所有行為構成的集合。
ｄ)%Ｓ × ×Ｓ。
定義７　運轉(ｒｕｎ)。運轉是由無限或有限多個狀態組成
的序列,可以被看做是系統的一次運行:$1 s0
Ａ
→
0 s１
Ａ
→
１
s２ ,其中s0(Ｉ,Ａｉ( ,(sｉ, Ａｉ, sｉ ＋１ )(%。由于ＴＬＡ 引入了啞
步,有限長的運轉可以通過啞步擴展為無限長的運轉。此外,
本文定義:$［ ｉ］ 1 sｉ,$［..ｉ］ 1 s0
Ａ
→
0 s１
Ａ
→
１ s２
Ａｉ
→
－１ sｉ －１ ,
(［ｉ..］ 1sｉ
Ａ
→
ｉ sｉ ＋１
Ａｉ
→
＋１ sｉ ＋２ 。
下面是在行為時序邏輯中重新定義表示系統運行集合的
符號:
定義８　系統運行的集合。對于一個標記轉移系統T＝
(Ｓ,Ｉ, ,%),一個有限的運轉$表示系統的一次未終止的運
行,而無限的運轉$表示系統的一次運行,有如下標記:
ａ)T*
$ 表示滿足標記轉移系統T 的有限運轉的集合,其中
s0(Ｉ,Ａｉ( ,(sｉ, Ａｉ, sｉ ＋１ )(%。
b)Tw
$ 表示滿足標記轉移系統T 的無限運轉的集合,其中
s0(Ｉ,Ａｉ( ,(sｉ, Ａｉ, sｉ ＋１ )(%。
c)(Ｓ, )*
$ 表示有限運轉的集合,其中Ａｉ( ,( sｉ, Ａｉ,
sｉ ＋１ )(%。
ｄ)(Ｓ, ) w
$ 表示無限運轉的集合,其中Ａｉ( ,( sｉ, Ａｉ,
sｉ ＋１ )(%。
T*
$ 和Tw
$ 表示系統從初始狀態開始的運行,而( Ｓ, )*
$ 和
(Ｓ, ) w
$ 表示系統從任意狀態開始的運行。
定義9　安全性。屬性Ｐ 是一個安全性,當且僅當($:
$(Tw
$: $｜≠Ｐ  (ｉ: ｉ≥0: (β: β(( Ｓ, ) w
$: $［..ｉ］ β｜≠
Ｐ)))。
定義１0　活性。屬性Ｐ 是一個活性,當且僅當(α: α(
T*
$: (β: β((Ｓ, ) w
$: αβ｜＝Ｐ))。
新的定義是為安全性和活性加入了初始狀態和狀態間轉
移關系的限制,將描述的運轉限定在符合系統基本要求的范圍
內,因為只有這樣的運轉對于系統而言才有意義。
根據安全性的定義可知,如果一個屬性Ｐ 不是安全性,那
么就是滿足^($·$(Tw
$: $｜≠Ｐ (ｉ: ｉ≥0: (β: β(
(Ｓ, ) w
$: $［..ｉ］β｜≠Ｐ))),即:$·$(Ｓw: ($｜≠Ｐ)∧(ｉ:
ｉ≥0: β: β(Ｓw: $［..ｉ］β｜＝Ｐ)。
根據活性的定義可知,如果一個屬性Ｐ 不是活性,那么就
是滿足^(α: α(T*
$: (β: β((Ｓ, ) w
$: αβ｜＝Ｐ)),即α:
α(T*
$: (β: β((Ｓ, ) w
$: αβ｜≠Ｐ)。
3　互斥協議的安全性
3．1　互斥概述
現代計算機系統的中心方案包括多道程序設計、多處理和
分布式處理,這些方案的基礎以及操作系統設計的基礎是并發
第5 期 趙夢龍,等：互斥協議的安全性分析 ·１４　８７　·　
　　
的,并發進程可以按照多種方式進行交互。系統中的眾多交互
進程可能需要競爭使用資源,如對Ｉ/O 設備的訪問、主存中的
一塊空間或者一個文件等。此類交互中產生的重要問題就是
互斥。
互斥的定義通常為［１0］ :一組并發進程中的一個或多個程
序段,因共享某一公有資源而導致它們必須以一個不允許交叉
執行的單位執行。也就是說,不允許兩個以上的共享該資源的
并發進程同時進入臨界區。互斥技術不但可以用于解決諸如
共享資源競爭等沖突,還可以用于進程間同步,使它們可以協
調合作［１１］ ,例如著名生產者/消費者問題:一個進程向緩沖中
寫入/添加數據,另外一個或若干個進程從緩沖中讀取數據。
3．2　安全性分析
假設一個系統Ｔ 中有兩個進程α和β,以及一個資源γ,進
行如下約定:
ａ)變量x＝0 表示進程α沒有占據資源γ;
b)變量x＝１ 表示進程α占有了資源γ;
c)變量y＝0 表示進程β 沒有占據資源γ;
ｄ)變量y＝１ 表示進程β 占有了資源γ;
ｅ)行為x: ＝0 將變量x 賦值為0,表示進程α釋放資源γ;
ｆ)行為x: ＝１ 將變量x 賦值為１,表示進程α占據資源γ;
g)行為y: ＝0 將變量y 賦值為0,表示進程β 釋放資源γ;
ｈ)行為y: ＝１ 將變量y 賦值為１,表示進程β 占據資源γ。
則存在圖１ 所示的狀態轉移圖。
假如資源γ是一個臨界資源,那么就必須遵循互斥協議:
不允許被兩個或兩個以上的進程同時占有資源γ。因此,就要
加入互斥性Ｍ:(x＝y)(x＝0)。
互斥性Ｍ可以用下面的狀態轉移圖２ 來表示。
圖１　系統的Ｔ 狀態轉移圖圖２　互斥性Ｍ的狀態轉移圖
由于狀態ｑ２ 是系統中唯一不滿足互斥性的狀態,所以可
以把互斥性Ｍ形式化地描述為
Ｍ＝｛$｜($(Tw
$)∧(ｉ≥0: sｉ≠ｑ２ )3
命題１　屬性Ｍ是安全性。
證明　$: $(Tw
$: $｜≠Ｐ (ｉ≥0: sｉ ＝ｑ２ ),取ｊ≥ｉ,
則β: β((Ｓ, ) w
$: $［..ｊ］β｜≠Ｍ。
因此,根據安全性的定義,屬性Ｍ是安全性。
證畢。
命題２　屬性Ｍ不是活性。
證明　系統中存在圖3 所示的有限運轉α:
圖3　系統Ｔ 中的一條有限運轉α
由于sｉ(α: sｉ ＝ｑ２ ,所以β((Ｓ, ) w
$,αβ｜≠Ｐ。
因此,屬性Ｐ 不是活性。
證畢。
由命題１ 和２ 可知,互斥協議屬于安全性而不是活性。它
只能保證系統不發生兩個進程同時使用同一個臨界資源的情
況,但不能保證某個進程一定能夠獲得一個臨界資源。
4　結束語
安全性和活性是兩類最基本的屬性,它們所確保的系統性
質是完全不同的。由于對于安全性和活性的驗證使用的是不
同的技術,所以區分一個屬性是安全性還是活性是十分必要
的。研究屬性的分類、定義和分析技術,對于系統的形式化分
析具有重要的意義。后續的研究可以在本文工作的基礎上,對
于一些典型的系統屬性進行分析,同時也可以探索安全性和活
性在實際系統驗證中的應用新途徑。
參考文獻：
［１］ CＨＥＮ Ｒｕｉ, ＬOＮG Sｈｉ-goｎg．Spｅcｉｆｙｉｎg coｎcｕｒｒｅｎｔ pｒogｒａｍ bａｓｅｄ oｎ
ＴＬＡ［C］//Ｐｒoc oｆ ｔｈｅ ２ｎｄ Ｉｎｔｅｒｎａｔｉoｎａｌ Coｎｆｅｒｅｎcｅ oｎ Ｍｅcｈａｎｉcａｌ
Ｄｅｓｉgｎ ａｎｄ Ｐoｗｅｒ Ｅｎgｉｎｅｅｒｉｎg．Ｚｕｒｉcｈ： Ｔｒａｎｓ Ｔｅcｈ Ｐｕbｌｉcａｔｉoｎｓ,
２0１４： ７9８-８0２．
［２］ ＰＡＲＫ Sｕｎg-ｈooｎ, ＫＩＭＹ Ｍ．Ｍｕｔｕａｌ ｅｘcｌｕｓｉoｎ ａｌgoｒｉｔｈｍ ｉｎ ｍobｉｌｅ
cｅｌｌｕｌａｒ ｎｅｔｗoｒｋｓ［ C］//Ｌｅcｔｕｒｅ Ｎoｔｅｓ ｉｎ Ｅｌｅcｔｒｉcａｌ Ｅｎgｉｎｅｅｒｉｎg, ｖoｌ
２１5．２0１3： 695-７0２．
［3］ ＬＡＭＰOＲＴ Ｌ．Ｔｈｅ ｔｅｍpoｒａｌ ｌogｉc oｆ ａcｔｉoｎ［Ｊ］．ＡCＭＴｒaｎｓ oｎ Ｐｒoｇｒaｍｍｉｎｇ
Ｌaｎｇｕaｇｅｓ aｎｄ Sｙｓｔｅｍｓ, １99４, １ 6(3)：８７２-9２3．
［４］ ＬＩ Ｊｕｎ-ｔａo, ＹＩＵ Ｚｉ-ｙｉ．Oｎ ａcｔｉoｎｓ oｆ ｔｅｍpoｒａｌ ｌogｉc oｆ ａcｔｉoｎｓ ［C］//
Ｐｒoc oｆ ｔｈｅ 3ｒｄ Ｉｎｔｅｒｎａｔｉoｎａｌ Coｎｆｅｒｅｎcｅ oｎ Ａｄｖａｎcｅｄ Coｍpｕｔｅｒ Ｔｈｅoｒｙ
ａｎｄ Ｅｎgｉｎｅｅｒｉｎg．Ｎｅｗ Ｙoｒｋ： ＩＥＥＥ Coｍpｕｔｅｒ Socｉｅｔｙ, ２0１0：
４４７４-４４７７．
［5］ CＨＡＵＤＨＵＲＩ Ｋ, ＤOＬＩGＥＺ Ｄ, ＬＡＭＰOＲＴ Ｌ, ｅｔ ａｌ．Ｖｅｒｉｆｙｉｎg ｓａｆｅｔｙ
pｒopｅｒｔｉｅｓ ｗｉｔｈ ｔｈｅ ＴＬＡ ＋pｒooｆ ｓｙｓｔｅｍ［C］//Ｌｅcｔｕｒｅ Ｎoｔｅｓ ｉｎ Coｍpｕｔｅｒ
Scｉｅｎcｅ, ｖoｌ 6１７3．Ｂｅｒｌｉｎ：Spｒｉｎgｅｒ,２0１0： １４２-１４８．
［6］ ＭＥＲＺ S．Ｐｒooｆｓ ａｎｄ pｒooｆ cｅｒｔｉｆｉcａｔｉoｎ ｉｎ ｔｈｅ ＴＬＡ ＋pｒooｆ ｓｙｓｔｅｍ
［C］//Ｐｒoc oｆ ｔｈｅ ２ｎｄ Ｉｎｔｅｒｎａｔｉoｎａｌ Ｗoｒｋｓｈop oｎ Ｐｒooｆ Ｅｘcｈａｎgｅ ｆoｒ
Ｔｈｅoｒｅｍ Ｐｒoｖｉｎg．２0１２： １6-２0．
［７］ 唐鄭熠, 李均濤, 李祥．行為時序邏輯中公平性的研究與完善
［Ｊ］．計算機應用研究, ２0１0, 27(5)： １７８８-１７9１．
［８］ COＵSＩＮＥＡＵ Ｄ, ＤOＬＩGＥＺ Ｄ, ＬＡＭＰOＲＴ Ｌ, ｅｔ ａｌ．ＴＬＡ ＋pｒooｆｓ
［C］//Ｌｅcｔｕｒｅ Ｎoｔｅｓ ｉｎ Coｍpｕｔｅｒ Scｉｅｎcｅ, ｖoｌ ７４36．Ｂｅｒｌｉｎ：Spｒｉｎgｅｒ,
２0１２： １４７-１5４．
［9］ ＢＡＩ Ｊｉｎ-ｓｈａｎ, ＴＡＮG Ｚｈｅｎg-ｙｉ, ＬＩ Ｊｕｎ-ｔａo, ｅｔ ａｌ．Ｌｉｎｅａｒ ｔｉｍｅ pｒopｅｒｔｉｅｓ
ｉｎ ＴＬＡ［ Ｊ］．ＪoｕｒｎaＩ oｆ Coｎｖｅｒｇｅｎcｅ Ｉｎｆoｒｍaｔｉoｎ Ｔｅcｈｎo-
Ｉoｇｙ, ２0１１, 6(１)： ２８４-２８８．
［１0］ ＷＡＮ Ｌｉａｎg, SＨＩ Ｗｅｎ-cｈａｎg．Spｅcｉｆｙｉｎg ａｎｄ cｈｅcｋｉｎg ｎｅｔｗoｒｋ pｒoｔocoｌ
bａｓｅｄ oｎ ＴＬＡ［C］//Ｐｒoc oｆ ｔｈｅ Ｉｎｔｅｒｎａｔｉoｎａｌ Coｎｆｅｒｅｎcｅ oｎ Ａｎｔｉ-
Coｕｎｔｅｒｆｅｉｔｉｎg, Sｅcｕｒｉｔｙ ａｎｄ Ｉｄｅｎｔｉｆｉcａｔｉoｎ．Ｗａｓｈｉｎgｔoｎ ＤC： ＩＥＥＥ
Coｍpｕｔｅｒ Socｉｅｔｙ, ２0１２： １８７-１95．
［１１］ ＺＨＡＮG Ｊｕｎ-ｍｉｎg, ＷＡＮG Ｋoｕ-ｗｕ．Ｔｈｅ ｓａｆｅｔｙ ａｎｄ ｌｉｖｅｎｅｓｓ pｒopｅｒｔｉｅｓ
oｆ ｔｈｅ ｎｅｔｗoｒｋ pｒoｔocoｌ bａｓｅｄ oｎ ＴＬＡ ［C］//Ｐｒoc oｆ ｔｈｅ Ｉｎｔｅｒｎａｔｉoｎａｌ
Coｎｆｅｒｅｎcｅ oｎ Ｉｎｆoｒｍａｔｉoｎ ａｎｄ Coｍｍｕｎｉcａｔｉoｎｓ Ｔｅcｈｎoｌogｉｅｓ．
Sｔｅｖｅｎａgｅ： Ｉｎｓｔｉｔｕｔｉoｎ oｆ Ｅｎgｉｎｅｅｒｉｎg ａｎｄ Ｔｅcｈｎoｌogｙ, ２0１3： ２１８-
２２２．
·１４８８· 計 算 機 應 用 研 究 　 第3２ 卷

網友評論 more

綜合安全論文最新內容

04-10