什么是广口蛙？

Wide Mouth Frog 协议是一种计算机网络验证协议，通常用于不安全的网络。它允许人们通过网络进行通信以验证彼此的身份，它还有助于防止重放攻击或窥探，并提供对任何更改的检测并防止任何不必要的读取。这可以通过 BAN (Burrows-Abadi-Needham) 逻辑来证明。然而，为了避免主动攻击，必须使用某种形式的消息认证或认证加密。

该协议可以在安全协议符号中指定如下，其中用户 A 使用服务器 S 向用户 B 验证自己：

其中用户A、用户B、可信服务器的身份分别为A、B、S。
用户 A 和服务器 S 生成的时间戳分别为 TS1 和 TS2。
只有 A 和 S 知道的对称密钥 KAS。
生成的对称密钥 KAB，它将是用户 A 和用户 B 之间会话的会话密钥。
只有 B 和 S 知道的对称密钥 KBS。

A  → S: A, {T{S1}, B, K{AB}}K{AS}
S  → B: {T{S2}, A, K{AB}}K{BS}

广口蛙协议

广口蛙协议的工作：

为了理解工作原理，让我们考虑一下 Wide-Mouthed-Frog 协议的例子：

M1 A → S: {T{S1}.B.K{AB}}SKey(A)  
M2 S → B: {T{S2}.A.K{AB}}SKey(B)

这里服务器与 A 和 B 共享两个不同的密钥，即 SKey(A) 和 SKey(B)；该协议的目的是在用户 A 和用户 B 之间建立一个会话密钥 K{AB}，并验证 A 到 B。之后，用户 A 创建一个会话密钥并将其与时间戳 TS1 一起定向到服务器；然后服务器将密钥连同新的时间戳 TS2 一起发送给用户 B。通常使用时间戳，以便用户可以获得他们收到的消息是最近创建的指示。应该注意的是，为了让这个机制通过和工作，不同用户的时钟需要同步；每个用户的时钟对于协议的安全性至关重要。

为了理解这个协议，我们需要看看如何在Casper中建模时间，Casper 语法的一些其他特性，以及选择要检查的系统的语用学。为此，让我们考虑运行该协议的四个不同系统。 FDR 发现系统 A 没有受到攻击，尽管它发现了对其他系统的三种不同攻击。大系统需要更多的时间来检查，所以一个实用的方法是从一个较小的系统开始，然后逐步向上。毫无疑问，我们检查的系统 D 已经在某种程度上进行了调整，以允许特定的攻击；但是，系统 A、B 和 C 是人们应该始终考虑的系统示例。

协议的大部分建模一般都很简单；下面给出了一些要点。

#Free variables
A, B : User
S : Server
SKey : User → SKeys
KAB : SEKey
TS1, TS2 : TimeStamp
InverseKeys = (SKey, SKey)

Casper 脚本中的大多数类型名称都可以由用户选择，但时间戳是一个例外。

时间戳在 Casper 中通过自然数建模。因此，与发送消息所需的时间相比，不对时间单位大小做出任何假设；同一时间单元内可能出现大量消息，也可能在连续消息之间传递一些时间单元。

#Processes
INITIATOR (A, S, KAB) knows SKey(A)
RESPONDER(B) knows Skey(B)
SERVER(s) knows SKey
#Protocol description
0. → A : B
1. A → S : {B, TS1, K{AB}}{SKey(A)}
[TS1==now or TS1+1==now]
2. S → B : {A, TS2, K{AB}}{SKey(B)}
[TS2==now or TS2+1==now]

Wide Mouth Frog 协议中的用户获取消息，他们可以检查他们收到的时间戳是否是最近的。它们是由获得前一条消息的用户完成的；如果检查失败，用户可以中止运行。

#Specification  
TimedAgreement(A, B, 2, [KAB])

要求是，如果响应者用户 B 完成了与用户 A 的协议运行，那么用户 A 应该在前面的两个时间单元内运行协议；此外，两个用户应该认可 KAB 的值，并且 A 和 B 的运行之间必须存在一对一的关系。所有这些对时间戳执行的测试都允许一次性单位的延迟每个，因此使两个时间单位的最大可能延迟。

然而，为了使这个规范有任何可能保持下去，在 S 检查消息 1 和发送消息 2 之间需要有一个可以忽略不计的延迟。

现在让我们看一下系统 A，考虑一个具有单个发起者用户 A 和单个响应者用户 B 的系统，两者都可以运行一次协议；使所有数据类型尽可能小并与该系统保持一致。一般对实际变量的描述比较简单；唯一的新功能是这里如何模拟时间：

#Actual variables
User A, User B, kcbt : User
mkcbt : Server
KAB : SessionKey
TimeStamp = 0 .. 0
MaxRunTime = 0

#System
INITIATOR(User A, mkcbt, KAB)
RESPONDER(User B)
SERVER(mkcbt)

#Functions
symbolic ServerKey

#Intruder Information
Intruder = kcbt
IntruderKnowledge = {User A, User B, kcbt, mkcbt, SKey(kcbt)}

这里我们假设入侵者可以产生所有时间戳；因此，它们不必包含在入侵者的初始知识中。因此，当使用 Casper 编译上述文件时，FDR 无法发现对后续系统的任何攻击。

现在，让我们看一下系统 B，考虑一个系统，其中用户 A 作为发起者可以同时运行一次协议。

#System  
INITIATOR(user A, mkcbt, kcbt)  
RESPONDER(user A)  
SERVER(mkcbt)

在这里，FRD 发现协议没有正确地将发起者用户 B 验证给响应者用户 A。因此，通过使用 FRD 调试器，我们可以找到如下所示的攻击形式。

M α.1 A → mkcbt: {B.0.KAB}SKey(A)
M β.2 Imkcbt → kcbt: {B.0.KAB}Skey(A)

攻击者只是将用户 A 的第一条消息重新运行回用户本身，他们将其解释为用户 B 启动的运行的消息 2。

现在，让我们看一下系统 C，其中响应者用户 B 可以顺序运行协议两次。

#System
INITIATOR(A, mkcbt, KAB)
RESPONDER(B) ; RESPONDER(B)
SERVER(mkcbt)

如果用户可以多次运行该协议，则可能会受到攻击；尽管通常情况下，攻击者可以使用第一次运行的信息来伪造第二次运行。

#System
INITIATOR(A, mkcbt, KAB)
RESPONDER(B)
RESPONDER(B)
SERVER(mkcbt)

现在，在此，FCR 告诉我们用户 A 未正确验证。因此，FDR 调试器可用于展示以下一些攻击，因为这些攻击违反了单射身份验证属性。

M α.1 A → mkcbt : {B.0.KAB}SKey(A)
M α.2 mkcbt → B : {A.0.KAB}SKey(B)
M β.2 Imkcbt → B : {A.0.KAB}SKey(B)

这里的问题是用户 B 认为他已经完成了两次协议运行，而用户 A 只想执行一次运行。这里攻击者基本上将mkcbt的消息重放给用户B，使用户B认为用户A正在尝试建立第二个会话。

现在，让我们看一下系统 D，这里攻击者可以打破两次单位限制。即用户 B 在用户 A 的相应运行之后完成了超过两个时间单元的运行。

TimeStamp = 0 . . 3
#System
INITIATOR(A, mkcbt, KAB)
RESPONDER(B)
SERVER(mkcbt) ; SERVER(mkcbt) ; SERVER(mkcbt)

检查系统后，FDR 会发现发起者用户 A 未按照上述时间规范进行身份验证。因此，使用调试器后，可以发现以下攻击。

M α.1 A → mkcbt : {B.0.KAB}SKey(A)
M α.2 mkcbt → IB : {A.0.KAB}SKey(B)
                   tock
M β.1 IB → mkcbt : {A.0.KAB}SKey(B)
M β.2 mkcbt → IA : {B.1.KAB}SKey(A)
                     tock
M γ.1 IA → mkcbt : {B.1.KAB}SKey(A)
M γ.2 mkcbt → IB : {A.2.KAB}SKey(B)
                     tock
M δ.1 Imkcbt → B : {A.2.KAB}SKey(B)

广口协议中的问题：

它需要一个全局时钟。
服务器 S 可以访问所有密钥。
会话密钥 KAB 的值由用户 A 确定。
它只能在有效的时间戳周期内重播消息。
用户 A 不确定用户 B 是否存在。
它是一个有状态的协议。