安全协议理论与方法-中国科学技术大学

1、2021/4/11安全协议理论与方法基于推理结构性方法2021/4/12Kailar逻辑可追究性的分析。内容：某个主体要向第三方证明另一方对某 个公式负有责任。2021/4/13Kailar逻辑的基本结构术语集合(基本语句)。 推理规则及公理。 基于的假设。2021/4/14Kailar术语集合A,B,C: 协议主体。M：由一个主体发送给另一个主体的消息。TTP: 可信第三方。Ki: 主体i的公开密钥。Ki-1:与K对应的主体i的秘密密钥。x,y:为命题。2021/4/15Kailar术语集合续Kailar逻辑的基本语句如下： 强证明 弱证明 签名认证 消息解释 声明断言 签名消息的接收(1)

2、信任2021/4/16Kailar术语集合续(1).强证明：A CanProof x如果对于任一主体B, A执行一系列操作之后没有向B泄漏任何秘密消息y(y不等于x)并且能够使B相信x，则称主体A能够证明命题x。包括以下两种情况： 可传递的证明1)不可传递的证明2021/4/17Kailar术语集合续可传递的证明如果A可向B证明x之后，B可向其他主体证明x的成立，则称A对于x的证明是可传递给B的。2）不可传递的证明如果B在A向其证明了x之后，并不能够向其他主体证明x是成立的，则称A对于x的证明是不可传递给B的。2021/4/18Kailar术语集合续(2)弱证明：A CanProof x to

3、 B主体A可在不泄漏任何秘密的前提下向一个特定主体B证明x的成立。可传递证明不可专递证明2021/4/19Kailar术语集合续签名认证Ka可用于认证A对消息的签名，而且毫无疑问地可以将A与用Ka-1加密的消息相联系。消息解释x in mx为m中的可被理解的一个域或联合域。通常可被理解的域指明文或主体拥有密钥的加密域。2021/4/110Kailar术语集合续声明断言：A says x 主体A声明x并对x及其所能够推导的公式负责，而且如果A对一个消息串负责，那么A也对每一个 子消息负责，即：A says (X,Y) = A says x2021/4/111Kailar术语集合续签名消息的接收：

4、A Received m SignedWith K-1A Received m SignedWith K-1: x in m A Received x SignedWith K-12021/4/112Kailar术语集合续信任: A Is TrustedOn xA 对公式x具有管辖权。信任可分为两个级别：全局信任：如果A是全局可信的, 那么对于所有主体有 A Is TrustedOn x。2) 非全局信任：如果A是非全局可信的, 那么对于所有主体有 A Is TrustedOn x by B。2021/4/113Kailar分析假设数字签名算法诚实性消息完整性服务器的有效性2021/4/114

5、Kailar分析假设数字签名算法 假设算法是完美的，不会被破解，可提供消息源的认证、消息内容的完整性和消息发送者的不可否认性。诚实性在非对称密码体制中，主体不会将其私钥泄漏给其他人而在对称密码体制中，主体不会伪装成与其共享密钥的主体。2021/4/115Kailar分析假设(3) 消息完整性 不可能用其他消息部分伪造签名消息或者计算出主体的私钥密钥并进而伪造签名。服务器的有效性语句A CanProof x 表明，在未来某个时间A可以发送一些消息来证明x，而一旦出现拒绝服务问题使得A无法发送消息以证明x的成立，那么此类问题将被消除以保证服务器的有效性。2021/4/116Kailar基本推理规则

6、一般规则1)联接2)蕴含3)信仰关系4)强弱证明关系5)全局与非全局的可信性可追究性规则1)签名2)信任2021/4/117Kailar基本推理规则一般规则联接Conj: A CanProve x; A CanProve yA CanProof (xy)蕴含Inf:A CanProve x; xyA CanProve y2021/4/118Kailar基本推理规则信仰关系(A Blieves x) iff(A CanProve x to A)A 相信x,当且仅当A能够对其自己证明x是成立的。强弱证明关系(S:C CanProve y)(A CanProve x)(S: C CanProve y

7、 to B)(A CanProve x to B)2021/4/119Kailar基本推理规则全局与非全局的可信性(S: C Is TrustedOn y) (A CanProve x)(S:C Is TrustedOn y by B)(A CanProve x to B)解释：如果C是为y所信任的，能够导致A能证明x,那么，在同样条件下，C通过B为y所信任可导致A能向B证明x的成立。2021/4/120Kailar基本推理规则可追究性规则签名当一个主体对一个消息签名之后，则签名消息就与主体进行了绑定并具有可追究性。Sign:A Receives (m SignedWith K-1);x in

8、 m; A CanProve (K Authenticates B)A CanProve (B Says x)2021/4/121Kailar基本推理规则信任Trust:A CanProve (B Says x); A CanProve (B IsTrustedOn x)A CanProve x如果A能够证明B声明了x,并且能够证明B对公式有管辖权，那么A能够证明公式x成立。2021/4/122Kailar逻辑的应用实例明确协议的可追究性目标。说明协议语句，并将其转化为逻辑公式。(关注签名)初始化协议假设条件。运用推理规则对形式化分析协议是否达成可追究性目标。如果未达成则意味着协议有漏洞。20

9、21/4/123Kailar逻辑的应用实例续CMP1 协议(电子邮件的不可否认性)AB:A,B,S,h(M), Kks,A,B,S,Mka-1kBS:A,B,S,h(M)kb-1, Kks,A,B,S,Mka-1kSB: A,B,S,Mka-1ks-1SA: A,B,S,h(M)kb-1,B,Mks-1本协议将反复执行3) 4)步，以保证A和B都能收到相应的消息。2021/4/124Kailar逻辑的应用实例续CMP1协议的目标形式化描述为：(G1) A CanProve (B received M)(G2) B CanProve(A Sent M)2021/4/125Kailar逻辑的应用实

10、例续协议语句的形式化：2)S Receives h(M)SignedWith kb-12”) S Receives h(M) SignedWith ka-13) B Receives h(M) SignedWith ka-1) SignedWith ks-14) A Receives (h(M)SignedWith kb-1 SignedWith ks-1 4”) A Receives (B,M) SignedWith ks-12021/4/126Kailar逻辑的应用实例续协议的初始假设I1: A,B CanProve (Ks Authenticates S)I2: A,S CanProve

11、 (Kb Authenticates B)I3: B,S CanProve (Ka Authenticates A)I4: A,B CanProve (S IsTrusted (S say)I5: A Says M A Sent MI6: B Says h(M) B Received h(M)2021/4/127Kailar逻辑的应用实例续I7:S Say (B,M) S Say (M had been sent to B)I8:B Receives h(M) M had been sent to B B Received M前四条是基本假设。后四条是扩展假设，合理性需要推敲。2021/4/1

12、28Kailar逻辑的应用实例续逻辑分析：1.由公式2) 和初始假设I2，应用签名规则可得：公式2) S Receives h(M)SignedWith kb-1初始假设A,S CanProve (Kb Authenticates B)A Receives (m SignedWith K-1);x in m; A CanProve (K Authenticates B)A CanProve (B Says x)结论：S CanProve (B Says h(M)2021/4/129Kailar逻辑的应用实例续2.由上述结论和初始假设I6,应用蕴含规则可得：I6: B Says h(M) B R

13、eceived h(M)蕴含规则：Inf:A CanProve x; xyA CanProve y结论：S CanProve (B Received h(M)2021/4/130Kailar逻辑的应用实例续3.由公式2”)和初始假设I3,应用签名规则可得：公式2) S Receives h(M)SignedWith ka-1I3: B,S CanProve (Ka Authenticates A)结论：S CanProve (A Says M)2021/4/131Kailar逻辑的应用实例续4.由上述结论和初始假设I5，应用蕴含规则可得：初始假设I5: A Says M A Sent MS C

14、anProve (A Sent M)2021/4/132Kailar逻辑的应用实例续5. 由公式3) 和初始假设I1,应用签名规则可得：3) B Receives h(M) SignedWith ka-1) SignedWith ks-1 I1: A,B CanProve (Ks Authenticates S)结论：B CanProve (S Says (M SignedWIthks-1)2021/4/133Kailar逻辑的应用实例续由上述结论和初始假设I4,应用信任规则可得：信任规则：Trust:A CanProve (B Says x); A CanProve (B IsTrusted

15、On x)A CanProve xI4:A,B CanProve (S IsTrusted (S say)结论：B CanProve (M SignedWith Ks-1)2021/4/134Kailar逻辑的应用实例续7. 对上述结论再次应用签名规则可得：结论：B CanProve (A Says M)8.由上述结论和初始假设I5,应用蕴含规则可得：结论 ：(G2)B CanProve (A Sent M)2021/4/135Kailar逻辑的应用实例续 证明G11. 同理，由公式4) 和初始假设I1、I4和I6，应用签名、信任和蕴含规则可得：结论： ACanProve (B Receive

16、s h(M)2021/4/136Kailar逻辑的应用实例续2. 由公式4”) 和初始假设I1,应用签名规则可得：公式4”) A Receives (B,M) SignedWith ks-1结论：A CanProve (S Says (B,M)2021/4/137Kailar逻辑的应用实例续3.对以上结果和初始假设I7，应用蕴含规则可得：I7: S Say (B,M) S Says (M had been sent to B)结论：A CanProve S Says (M had been sent to B)2021/4/138Kailar逻辑的应用实例续4.对以上结果和初始假设I4,应用信

17、任规则可得：I4: A,B CanProve (S IsTrusted (S say)信任规则： Trust:A CanProve (B Says x); A CanProve (B IsTrustedOn x)A CanProve x结论：A CanProve (M had been sent to B)2021/4/139Kailar逻辑的应用实例续由前述结论A CanProve (B Receives h(M)A CanProve (M had been sent to B)应用联接规则可得：A CanProve (B Receives h(M) M had been sent to B)对以上结果和初始假设I5,应用蕴含规则可得：(G2) A Ca