（补充）SPAN+AVISPA for Verifying Cryptographic Protocols

本文是对视频教程的重学习。整理自己的理解。

入侵者（I）先验知识：

｛A，B，Ka，Kb，Ki，Ki-1｝

I 能 获取每次信息传递的全部内容。（能不能推导出来看设计的如何了）

达到的目标：

1.信息的机密性。公钥加密，私钥解密 保证信息的机密性。

2.认证

消息认证：如果A知道是谁创建的消息m，则称A能认证m。电子签名：私钥加密、公钥解密。（ID,{ID}K-1） 比较ID是否一样。

agent认证：如果一次成功的协议会话后，A知道他和B在通过协议交互。则代理A能认证代理B

3.freshness：在协议会话期间message是新鲜的

协议解读（实现B给A传消息）

protocol 0

B -> A : B，s

显然，入侵者，能够容易的得到s

protocol 1

B -> A : ｛B，s｝Ka

Ka是公钥，I 能够伪装成B

protocol 2

B -> A : B，｛s｝Kb-1

达成：消息认证

但 I 知道B的公钥，可以推导出s

protocol 3

B -> A : ｛B，s，｛s｝Kb-1｝Ka

达成：信息的机密性；消息认证

但是没有freshness

I 能获得｛B，s，｛s｝Kb-1｝Ka 全部信息，等2000年后再发给A

agent 认证 未达成

protocol 4

Na ：fresh number

1. A -> B : ｛A，B，Na｝Kb
2. B -> A : ｛A，B，Na，s｝Ka

达成：信息的机密性、新鲜性、A知道s是B建立的（Na只有B的私钥能推导出来）、会话成功后A认证B。

protocol 5（使用对称密钥）

1. A -> B : ｛A，B，Na｝Kab
2. B -> A : ｛A，B，Na，s｝Kab

DY模型：

1. 加密是安全的
2. 入侵者有对整个网络的控制权

安全目标属性：

可参考文章：形式化分析工具AVISPA（三）学习User micro-manual of AVISPA 1.5 声明安全属性

secret(information,identifier,agents-set)

witness(X,Y,identifier,information)

request(Y,X,identifier,information)

secret（）infor 是 agents 保密的信息 标签为identifier

wrequest（） Y想验证 infor 是X构建的，标签为identifier

witness（） X希望infor能够被认证

参考：

设计一个交换协议

A----------------------------T----------------------------B

方案1:

1. A -> T : ｛Kab｝_Kat
2. T -> B : ｛Kab｝_Kbt

入侵流程：

1. A -> T : ｛Kab｝_Kat 被 I 监听
2. I（A） -> T : ｛Kab｝_Kat
3. T -> I : ｛Kab｝_Kit I可推导出Kab

方案5（达成安全及相互认证）：

1. A -> T : ｛A，B，Kab，Na｝_Kat
2. T -> B : ｛B，A，Kab，Na｝_Kbt
3. B -> A : ｛A，B，Na，Nb｝_Kab
4. A -> B : ｛A，B，Nb｝_Kab

方案6（对5的优化）：

1. A -> T : ｛B，Kab｝_Kat
2. T -> B : ｛A，Kab｝_Kbt
3. B -> A : ｛B，Nb｝_Kab
4. A -> B : ｛Nb｝_Kab