Gavin Lowe, 1997

理想状态下，我们希望世界上的协议都是这样的，一对一认证：

image-20230619162659073

但是实际上，显示网络空间中的实体与协议是这样的：

image-20230619162747437

很容易出现这种情况：

image-20230619162818130

我们希望一一对应，相互认证：

image-20230619162923180

于是出现了以下四个认证属性（authentication），逐渐变强。

存活性（Aliveness）

发起者A认为与B完成了一轮协议会话，并且认为B为响应者，如果B确实曾经执行过该协议，则称协议对发起者A提供B的存活性认证，在满足存活性的情况下，

  • 不要求B是与A执行的该协议**（对象不要求）**
  • 并且也不要求B是最近执行的改协议，只要B曾经参与过协议执行即可**（时间不要求）**
∀a b i. Claim_commit(a, b, <> )@i
`	⇒ (∃j id.Create_B(b, id)@j ∨ Create_A(b, id)@j)
	∨(∃X r.Rev(X)@r ∧ Honest(X)@i)

存活性的要求最低，但是也有失效的可能，比如受到**反射攻击（reflection attack）**时。如下图这个协议，可能B会不参与协议：

image-20230612170414022

Tamarin验证如下：

image-20230612173207694

弱一致性（Weak agreement）

发起者A 认为与B完成一轮协议会话，并且认为B为响应者，如果B确实曾与A执行过该协议，则称协议发起者A提供B的弱一致性，满足弱一致性时，

  • B与A执行过该协议，但是不一定作为响应者**（对象半要求）**
  • （时间不要求）
∀a b i. Claim_commit(a, b, <> )@i
	⇒ (∃j.Claim_running(b, a, <> )@j)
	∨(∃X r.Rev(X)@r ∧ Honest(X)@i)

a,b交流过，但是不要求它们扮演正确的角色

下图存活性成立，弱一致性不成立。攻击者可以修改第一条消息中未受保护的标识符A，换成C，导致B认为自己在与A通信。

image-20230612163837722

Tamarin验证如下：

image-20230612164054692

非单射一致性 (No-injective agreement)

发起者A认为与响应者B完成了一轮协议会话，如果B确实作为响应者曾与A执行过该协议，并且两个主体对变量集ds中的所有变量的值都是统一认可的，则称协议发起者A提供B在变量集ds上的非单射一致性。

那么满足非单射一致性的协议中，发起者A的协议轮和响应者B的协议轮不要求一一对应，有可能A发起了两次会话，但是B只运行了一次，另一次由攻击者重放第一轮会话冒充B完成，也有可能A只发送了一次会话，但攻击者重放第一轮会话冒充A， 让B运行两次，另外，有些协议不满足非单射一致性是因为攻击者成功误导两个参与主体，使得两个主体在协议运行结束后，变量集ds中的某些变量的值不同。

∀a b t i. Claim_commit(a, b, <A, B,t> )@i
	⇒ (∃j.Claim_running(b, a, <A, B,t> )@j)
	∨(∃X r.Rev(X)@r ∧ Honest(X)@i)

单射一致性(Injective agreement)

发起者A认为与响应者B完成了一轮协议的会话，如果B确实作为响应者曾与A执行过该协议，并且两个主体对变量集ds中的所有变量的值都是统一认可的，并且A的每一轮会话都是唯一对应B的一轮会话，则称协议对发起者A提供B在变量集ds上的单射一致性。也称作强一致性，在电子商务相关的协议中A和B的协议之间的一一对应的关系非常的重要的。

所以说上面的区别主要就是在发起者A有没有存在唯一对应的应答。

∀a b t i. Claim_commit(a, b, <A, B,t> )@i
	⇒ (∃j.Claim_running(b, a, <A, B,t> )@j ∧ j < i
	∧¬(∃a2b2i2.Claim_commit(a2, b2, <A, B,t> )@i2
	∧¬(i2 = i)))
	∨(∃X r.Rev(X)@r ∧ Honest(X)@i)

下图满足非单射一致性，不满足单射一致性，攻击者可以重放消息。

image-20230612161442742

Tamarin验证如下：

image-20230612162152502