文档介绍：安全协议理论与方法
基于推理结构性方法
Kailar逻辑
可追究性的分析。
内容:某个主体要向第三方证明另一方对某
个公式负有责任。
Kailar逻辑的基本结构
术语集合(基本语句)。
推理规则及公理。
基于的假设。
Kailar术语集合
A,B,C…: 协议主体。
M:由一个主体发送给另一个主体的消息。
TTP: 可信第三方。
Ki: 主体i的公开密钥。
Ki-1:与K对应的主体i的秘密密钥。
x,y…:为命题。
Kailar术语集合续
Kailar逻辑的基本语句如下:
强证明
弱证明
签名认证
消息解释
声明断言
签名消息的接收
信任
Kailar术语集合续
(1).强证明:A CanProof x
如果对于任一主体B, A执行一系列操作之后没有向B泄漏任何秘密消息y(y不等于x)并且能够使B相信x,则称主体A能够证明命题x。包括以下两种情况:
可传递的证明
不可传递的证明
Kailar术语集合续
可传递的证明
如果A可向B证明x之后,B可向其他主体证明x的成立,则称A对于x的证明是可传递给B的。
2)不可传递的证明
如果B在A向其证明了x之后,并不能够向其他主体证明x是成立的,则称A对于x的证明是不可传递给B的。
Kailar术语集合续
(2)弱证明:A CanProof x to B
主体A可在不泄漏任何秘密的前提下向一个特定主体B证明x的成立。
可传递证明
不可专递证明
Kailar术语集合续
签名认证
Ka可用于认证A对消息的签名,而且毫无疑问地可以将A与用Ka-1加密的消息相联系。
消息解释x in m
x为m中的可被理解的一个域或联合域。
通常可被理解的域指明文或主体拥有密钥的加密域。
Kailar术语集合续
声明断言:A says x
主体A声明x并对x及其所能够推导的公式负责,而且如果A对一个消息串负责,那么A也对每一个子消息负责,即:
A says (X,Y) => A says x