第5 章
基于行为模型的密码协议验证 
本章用行为模型(actionmodel)来扩展认知逻辑以构建语言来描述并验证
密码协议。本章还是采用第4章的实例作为分析验证的例子。
5.1　协议的语言LA,B 
Cryp 
本节用行为模型来描述这个实例,令语言为LA,B 
Cryp,其中Cryp表示密码学
(cryptography),A 是协议全体主体集,B .A 是主体集中一个子集,表示在认
知状态中将被分析的参与这个协议的主体。这个语言中的命题由has、const、tg 
构成,has表示主体拥有的消息,const表示主体可以从自身的信息集构造的消
息,tg表示为密码协议中已经完成的行为做标记。用A表示行为集。
5.1.1 协议语言LA,B 
Cryp的语法
本章对协议中的消息集M的定义沿用定义4.1,即m ::=a|n|k|mk|(m , 
m )(m ∈M)。
定义5.1:本协议基本命题 在这个密码协议系统中,用ΦA Cryp作为基本命
题p 的集合,基本命题p 定义为
p::=hasam|constam|tg(σ) 
其中,a∈A ,m ∈M,σ∈A。hasam 表示主体a 拥有消息m ,constam 表示主体
a 从自己的信息集构造m ,tg(σ)表示行为σ 被标记。令ΦI,ΦI- ,Φtg是ΦA Cryp的
子集,分别表示上述3种命题的集合。
下面定义行为模型。根据文献[160]的思想,一个行为的执行需要的条件
称为前提条件(precondition),没有相应的前提条件,这个行为是不能被执行的。
在这个系统中,所有的前提条件属于ΦA Cryp,它是语言ΦA,B 
Cryp的一部分。一个行为
执行后成立的命题称为后置条件(postcondition),后置条件表明行为执行后知

64 
识的变化,后置条件分为两部分,一个是PosI 表明主体信息集的变化,另一个
是PosAL表明行为标记的变化(记录主体完成的行为)。基于逻辑语言LA,B 
Cryp,一
个行为模型是一个元组A=(A,~a ,Pre,PosI,PosAL),其中A是一个非空的有
限的行为集,对所有的a∈B,~a 是一个等价关系。Pre:A→ΦA Cryp为每一个行
为指派一个前提条件。应用文献[160]的思想处理后置条件,函数Φ →L是对L 
的一个替换,是基本的逻辑语言到它的变体的一个映射。SUB是substitution 
的缩写,SUB(L)被看作从Φ(命题)到L(语言)的一个替换集。因此,PosI:A→ 
SUB(ΦA,B 
Cryp),后置条件是语言LA,B 
Cryp的一个替换,对任意的p∈ΦI,σ∈A,有性质
PosI(σ)(p)∈ΦI∪{ , }。PosAL:A→SUB(ΦA,B 
Cryp),对任意的p∈ΦAL,σ∈A, 
有PosAL(σ)(p)∈ΦAL ∪{ , }。用“m ∈Ia (Ia 表示a 的信息集)”替换
“hasam ”映射到,同时,在σ 行为执行后消息m 增加到a 的信息集。用“σ+ ” 
来标记当前行为对替换映射tg(σ)到,同样地,用“σ- ”来标记之前的行为对替
换映射tg(σ)到。在后面的分析过程中,将用这些替换来形式化所有的后置
条件。定
义5.2:本协议语言LA,B 
Cryp的语法 给定主体集A 和基本命题集ΦA Cryp,协
议语言LA,B 
Cryp的语法归纳定义为
φ::= |p|..φ|φ ∨φ|Kaφ|[α]φ 
α::=(A,σ) 
其中,p∈ΦA Cryp,a∈A,σ 是行为模型A中的一个行为。[A,σ]φ 意思是在A中
的行为σ 执行后,φ 成立。
5.1.2 协议语言LA,B 
Cryp的语义
语言LA,B 
Cryp的模型M是一个元组
M=(W ,{Ra}a∈B ,I,AL) 
其中,W 是一个非空的可能世界集,Ra 是对所有的a∈B 在W 上的二元关系。
I 是信息集,Iw ,a 表示在世界w ,主体a 的信息集,也就是说I:W ×A→P(M)。
AL表示行为标签,即AL:W →P(A)。对任意的σ∈A,tg(σ)意味着在行
为集A的行为σ 已经被标记。I 和AL是对应的基本命题的值。若m ∈Ia ,则
hasam 成立。m 是a 的拥有集的消息,可以是通过接收得到的也可以是初始分
配的,消息m 也可以由主体从它的信息集中的信息构造的,构造规则遵循第4 
章介绍的密码学构造规则,即
mk 
mk mkk 
m mm' 
(m ,m') (m ,m') 
m (m ,m') 
m'

65 
令协议语言LA,B 
Cryp的模型为M,基本命题的语义如下: 
M,w hasam 当且仅当m ∈Iw ,a ; 
M,w constam 当且仅当m ∈Iw ,a ; 
M,w tg(σ) 当且仅当σ∈AL(w ); 
第一条是说如果模型在世界w 满足主体a 拥有消息m ,当且仅当,消息m 
属于a 在世界w 的信息集。第二条说主体a 可以构造消息m 在(M,w ),当且
仅当m 可以从他的信息集Iw ,a 推导,“m ∈Iw ,a”表示m 属于集合Iw ,a 的推导集
(Iw ,a 表示从集合Iw ,a 推导出来的信息集)。第三条表明,tg(σ)在(M,w )成立, 
当且仅当σ 在(M,w )被标记。
更新模型令协议语言LA,B 
Cryp的模型为M,A是行为模型,更新模型
M..A=(W',{R'a}a∈B ,I',AL') 
被定义为
W'={<w ,σ>|M,w Pre(σ)} 
R'a ={<w ,σ>,<v,σ'>|w R'av 和σ~aσ'} 
I'(<w ,σ>,a)={m|M,w PosI(σ)(hasam )} 
AL'(<w ,σ>)={β|M,w PosAL(σ)(tg(β))} 
定义5.3:本协议语言LA,B 
Cryp的语义 给定主体集A 和基本命题集ΦA Cryp,协
议模型为M=(W ,{Ra}a∈B ,I,AL)且状态w ∈W ,本协议语言LA,B 
Cryp的语义定义
如下: M,w ° 当且仅当M,w ; 
M,w ..φ 当且仅当M,w φ; 
M,w φ∨ψ 当且仅当M,w φ 或者M,w ψ; 
M,w Kaφ 当且仅当对任意一个w'∈W ,若wRaw',则M,w'φ; 
M,w [A,σ]φ 当且仅当若M,w Pre(σ),则M..A,<w ,σ>φ。
5.2　协议形式化
5.2.1 形式化密码协议中的基本问题
1.协议形式化描述形式 
这里用Crypto来表示该密码协议的行为模型。事实上协议的运行是一系
列动作的执行。在密码学中,协议被描述为这样的形式: 
a→b:m 表示主体a 发送消息m 给b, 其中,m ∈M

66
2.实例化
行为模式是协议执行中的一个重要部分。通常用instatiationθ 实例化行
为模式,θ 为任意的一个实例。instatiationθ 是一个从协议参数到它们各自的
域的映射。一个协议的执行有几个实例的相互交错。在该系统中,应用Θ 来表
示实例集,协议的参数是有限的,因此Θ 集的元素也是有限的。
3.网络环境
参照文献[161],假定该协议的网络由输入缓冲器(inputbuffer)和输出缓
冲器(outputbuffer)构成。将这两部分看作两个特殊的主体In和Out。可信
任的主体消息仅能发送给In,攻击者或入侵者能够窃听In的信息。可信主体
仅能接收来自Out的消息。
4.验证模型
验证模型是该协议要达到的目标模式。在协议运行结束后,目标公式.(. 
∈ΦA,B 
Cryp)成立,形式化验证模型如下: 
M ∧ θ∈Θ[CryptoIntr,σ(θ)].(θ) 
其中,M是之前定义的模型,包括所有初始假设条件和所有主体的初始认知信
息。CryptoIntr表示行为模型,这个模型中的行为包括入侵者的行为。Intr表示
入侵者(intruder)。σ 是行为模型A 中的行为,通常是行为序列中的最后一个。
. 是ΦA,B 
Cryp中的公式,或者是静态认知公式或者是命题公式。
∧ θ∈Θ[CryptoIntr,σ(θ)].(θ) 
表示包括入侵者的行为的模型CryptoIntr中所有的行为执行完成之后,公式. 成
立。这是协议的目标模型的表达式。
5.2.2 形式化行为模型
在协议的运行中语言模型的变化依赖于行为的执行。也就是说,行为的执
行导致模型的变化。因此,首先给出行为模型。前面定义了初始化模型M和
行为模型CryptoIntr。假定Ag 表示协议中主要被分析的主体集,入侵者
(intruder)T (T ∈Ag)执行入侵行为。所以,在这个系统中,主体集A =Ag∪ 
{In,Out}和B =Ag。入侵者的行为和协议的行为要求是根据入侵者模型和来
源于在CryptoIntr模型中行为集A的协议规定的行为。
在协议中,a→b:m 表示a 发送消息m 给b。这个行为分成'send'(σ)a→ 
In:m 和r' eceive'(δ)Out→b:m 两部分。执行这个行为的前提是a 可以从他的
信息集构造m :Pre(σ)=constam 。行为σ 的后置条件是PosI(σ)=m ∈IIn。用

σ+,

σ-来标记刚刚完成的行为和这个行为之前的行为。同样地,行为
δ 
的前提
条件为Pre(=atm。规定缓冲器本身不能构造新的信息。
δ 
的后置条件

δ)hs
为Posδ)=m∈Ib 。(u) (o) 

I(

在这个网络模型中,假定入侵者可能窃听所有缓冲器的信息。因此,入侵者
T 
的行为是In→T:
m 
或者T→Out:m。也就是说,一方面入侵者可以从输入缓
冲器获取信息(em),另一方面他可以把信息放入输出缓冲器()。这个

takfakem
行为描述如表51所示
。


.

表5.入侵者
T 
的行为模型

1 

Action 
Direction 
Mesage 
Pre 
PosI 
PosAL 
takem 
In→
T m 
hasInm 
m∈IT 
— 
fakem 
T→Out 
m 
constTm 
m∈IOut — 

在这个系统中,主体只能区分他自己完成的行为,别的主体的行为不可区
分的。用~ 
a 
来表示任意主体
a 
不可区分的行为,~ 
T 
表示入侵者不可区分的
行为。协议的模型M=(
W 
,{Ra 
}I,的初始状态描述如下。

a∈
B 
,AL)

W 
是一个非空的可能世界集。

I 
是主体的信息集。一个主体的信息集总是基于一个确定的世界。因此, 
主体
a 
和他的信息集
I 
定义一个世界w,通常地,写作I(w,。在初始状态,规
定缓冲器是空的,因此对所有的w∈
W 
,在初始状态有I(w,Ina)
)
=I(w,Out)=. 。
Ra 
如果wRa当且仅当I(w,a)Ra 
表示对主体
a 
来说是等价关系,

v, a)=I(v,
a 
不能区分
w 
和v。

AL在初始状态,对所有的w∈
W 
,令AL(w)=. 。

在后面分析具体协议时,将应用上面的形式化方法。

5.3 
　协议分析
沿用第4章的例子。在一个不安全的网络中,甲想发送给乙一个秘密消息
m。他们只有自己的密钥。假定甲作为发送者(S),乙作为接收者(R)。发送
者有自己的密钥ks,接收者有自己的密钥kr 
。他们只能解密自己加密的数据。
协议描述如下: 

(1)S→R:ms 

(2)R→S:msr 

67

(3)S→R:mr 
在第(1)步,发送者用k加密
m 
得到{m},为了简洁,写作ms。发送者将

ks 

ms 
发送给接收者。接收者收(s) 到后,用k加密ms 
得到ms。再把msr 
返回给发
送者,发送方解密ms得到mr 并发送到(r) 接收者。接收者可(r) 以解密mr 
并得到
。最后,
m 
从
S 传输(r) 到R。应用的加密有可交换的性质,即msr 
=mrs(加密信息(m) 时密钥的使用顺序的改变不改变加密结果)。这里,密钥可以是对称的,也可
以是非对称的公私钥对密钥。下面形式化这个协议。在协议中,消息集
M 
= 
{s,
r 
,m,ms,
r 
,},Ag={S,R,
T 
},其中
S 
是发送者,
R 
是接收者,
T 
是kkmsmrR,IOu着重分析的协议参与者

入侵者。协议的全体主体集为A={S,T,n,t}, 
集合B=Ag={S,R,
T 
}。首先给出初始
模型图5.然后根据协议行为的执行的运

1, 
行过程形式化协议。在初始状态,只有
S 
有信息
m 
其他人没有m,初始模型中表明
了哪一个主体拥有m。根据Iw,
S 
,Iw,
R 
, 
Iw,
T 
,如果主体在那个世界有
m 
就出现在
那个世界。在图5.实线表示这两端的

1中, 
世界对
S 
是可以区分的(其余是不能区分
的),虚线表示两端的世界对
T 
是可以区分图5.协议的初始模型
的,点线表示两端的世界对
R 
是可以区分
1 
的。因此,在初始状态满足:M,
S 
hasSm∧..hasRm∧..hasTm。

协议的行为模型形式化如表5.

2所示。

表5.协议的行为模型形式化

2 


Action 
Direction 
Mesage 
Pre 
PosI 
PosAL 
σ1 S→In ms 
constSms 
ms 
∈IIn σ+1 
δ1 Out→
R 
ms 
hasOutms 
ms 
∈IR 
δ+1 
σ2 R→In msr 
constRmsr 
msr 
∈IIn δ-1 ,σ+2 
δ2 Out→
S 
msr 
hasOutmsr 
msr 
∈IS 
δ+2 
σ3 S→In mr 
constSmr 
mr 
∈IIn δ-2 ,σ+3 
δ3 Out→
R 
mr 
hasOutmr 
mr 
∈IR 
δ+3 

如表5.行为σ1 表示
S 
将消息ms 
n,前提条件是
S 
能够构

2所示, 发送到I

68

造ms,后置条件是ms 
属于In,同时标记σ1 这个行为。第2行δ1 表示
R 
从
Out接收到消息ms,前提是Out有消息ms,这个行为执行后
R 
有消息ms,同
δσ+” δ”,

时标记δ1。第3行的“1,中“表示
R 
执行的当前行为是σ2,之前的一
个行为是δ1。这里将协议参(2) 与主体(1) S,
R 
的当前行为和前一个行为都做了

标记。
3中添加了来自入侵者(

表5.T)的操作。假设入侵者是一个弱的入侵者。
除了窃听他无法构造任何信息,因为没有密钥,所以只能从缓冲区中接收所有
消息并传输到输出缓冲器。

表5.包括入侵者行为的行为模型

3 

Action 
Direction 
Mesage 
Pre 
PosI 
PosAL 
σ1 S→In ms 
constSms 
ms 
∈IIn σ+1 
takems 
In→
T 
ms 
hasInms 
ms 
∈IT 
— 
fakems 
T→Out ms 
hasTms 
ms 
∈IOut — 
δ1 Out→
R 
ms 
hasOutms 
ms 
∈IR 
δ+1 
σ2 R→In msr 
constRmsr 
msr 
∈IIn δ-1 ,σ+2 
takemsr 
In→
T 
msr 
hasInmsr 
msr 
∈IT 
— 
fakemsr 
T→Out msr 
hasTmsr 
msr 
∈IOut — 
δ2 Out→
S 
msr 
hasOutmsr 
msr 
∈IS 
δ+2 
σ3 S→In mr 
constSmr 
mr 
∈IIn δ-2 ,σ+3 
takemr 
In→
T 
mr 
hasInmr 
mr 
∈IT 
— 
fakemr 
T→Out mr 
hasTmr 
mr 
∈IOut — 
δ3 Out→
R 
mr 
hasOutmr 
mr 
∈IR 
δ+3 

5.4 
　协议验证
5.1 
协议的目标模型
4.
在初始状态,
S 
和
R 
有自己的密钥,但只有
S 
才有秘密消息m。协议目标
是所有动作执行完成后,
R 
有秘密消息m,而
T 
没有。因此,得出目标模型。
目标1:在最后一个行为δ3 执行后,
R 
有秘密消息m。

69

70 
M ∧ θ∈Θ[CryptoIntr,δ3(θ)]KAgconstRm (θ) 
目标2:在初始状态T 没有m ,在最后一个行为δ3 执行后,T 仍然没有m 。
M ∧ θ∈Θ..hasTm (θ)→[CryptoIntr,δ3(θ)]KAg ..constTm (θ) 
如果协议满足目标1和目标2,那么该协议是安全的。
5.4.2 协议的验证
命题1:对于任何一组消息项M,以及任意秘密消息m :没有密钥k,如果
m .M-,则m .mk ∪M。
从构造规则来看,如果主体有mk 和相应的密钥k,则可以构造m 。没有密
钥k,如果m 不能从M推导(能从M推导得出的集合表示为M-),则即使mk 并
到M集,还是不能推导得出m ,因为缺少前提密钥k。根据这个命题,T 不能计
算秘密消息m ,因为他的消息都来自输入缓冲器,从表5.3的PosI 列可以看出, 
他没有相应的密钥k。在这个系统中,主体的消息集的元素总是增加而不是减
少的。因此得出命题2。
命题2:对任意消息m 和任意主体a,有
M constam →[CryptoIntr]constam 
命题3:目标2在协议的运行过程中总是真的。
在初始状态,只有S 有消息m ,其他人没有m 。当然T 不可能有m ,因为
协议还没有运行,什么行为也没有做。
现在证明目标2在协议的运行过程中总是真的。
假设存在一个世界w 不满足目标2, 
M,w ..hasTm →[CryptoIntr]..constTm 
如果上面这个公式成立,那么就存在一个动作序列σ1,σ2,…,σn (σi∈A), 
使得
M,w ..hasTm ∧[CryptoIntr,σ1]…[CryptoIntr,σn]constTm 
然而,从表5.3可以看到,在任何一个状态,T 都没有m ,所以
M,w ..hasTm ∧[CryptoIntr,σ1]…[CryptoIntr,δ3]..constTm 
因此,假设是不成立的。
入侵者仅能从输入缓冲器得到信息。如果m ∈IIn,那么m ∈IT 。从表5.2 
或表5.3可以列出输入缓冲器的信息集
1≤∪i≤n
I(wi,In )={ms,msr,mr}

因此,
T 
拥有的消息都是加密数据,没有相应的密钥k,他不能计算并得到
秘密消息m。因此目标2是满足的。
命题4:目标1在初始状态不成立,在协议的最后一个行为δ3 完成后,目标
1成立。
证明:在初始状态,
R 
没有m,
R 
只有kr 
。协议的所有行为执行后,根据
表5.
R 
的信息集为

3,
∪I(wi,R)={ms,msr 
,mr}


1≤i≤
n 

因此,
R 
有kr 
和mr 
,根据构造规则,
R 
可以构造出m,即constRm。因此, 
协议的所有行为执行后,得到下式: 
M 
[tkatkatkaδ3]osRm

σ1][e][δ1][e][δ2][e][

afke][σ2][afke][σ3][afke][cnt
因此,目标1和目标2得证。此协议是满足安全要求的。

5.5 
　本章小结
本章应用文献[75,的思想用行为模型扩展认知逻辑形成动态认知逻

160]
辑,描述、分析并验证一个具体的密码协议。这个协议是两个主体,要在一个不
安全的网络中传送一个秘密消息,它们仅有自己的密钥,只能解密自己加密的
消息。本章给出了描述这个协议的语言的语法和语义。用行为模型来刻画协
议的行为,行为的执行导致模型的变化,更新模型描述了模型的转换。精确地
详细地模式化协议的每一步。从实际意义上来说,逻辑表示就是逻辑分析。根
据安全要求,给出协议的安全目标,通过分析和证明,这个协议满足预设的目
标,这个协议是安全的。

71