什么是“大嘴蛙”呢？

Wide Mouth Frog协议是一种用于不安全网络上的计算机网络验证协议。 它允许人们通过网络进行通信，从而相互验证身份。此外，它还有助于防止重放攻击，以及防止未经授权的窥探行为。同时，它还能检测任何篡改行为，并防止不必要的读取操作发生。 这可以通过BAN（Burrows–Abadi–Needham）逻辑来证明。 不过，为了避免主动攻击，必须采用某种形式的消息认证或加密技术来确保数据的安全性。

该协议可以用安全协议表示法来如下描述：用户A通过服务器S来验证自己与用户B之间的身份关系。

• 用户A、用户B以及可信服务器的身份分别对应于A、B和S。
• 用户A和服务器S生成的时间戳分别为TS1和TS2。
• 一种对称密钥KAS，只有A和S知道其存在。
• 生成的对称密钥KAB，将会成为用户A与用户B之间通信过程中的会话密钥。
• 这是一种对称密钥KBS，只有B和S知道它的存在。

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]

那些用户们宽口蛙协议如果获得了消息，他们可以检查所接收到的时间戳是否是最新的。这一操作由获取了之前消息的用户来完成；如果检查失败，那么用户就可以终止该流程。

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

要求是：如果响应用户B完成了该协议的某个运行过程，而用户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发送了最初的消息，而用户A则将其视为由用户B发起的第二次消息。

现在，让我们来看看系统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是否存在。
• 这是一种具有状态维护功能的协议。