导航：安全管理网>> 安全论文>> 综合安全论文>>正文

互斥协议的安全性分析

文档作者：赵梦龙１唐郑熠２万良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

综合安全论文最新内容

05-04