Modified Wide-Mouthed-Frog Protocol

The second example illustrates the `gap' that exists between an `idealized' version of a protocol and its actual implementation.

Table 4-b shows a modified version of the `wide-mouthed-frog protocol' (table 4-a; see also [1]). The role of the two timestamps in the original protocol is now played by a nonce, thus removing the need for synchronized clocks. However, an extra (first) message has to be sent.

 
Table 4:  The wide-mouthed-frog protocol

When this protocol is analysed through the BAN-logic, the messages have to be idealized and the initial assumptions have to be listed. The first message is omitted, since it does not contribute to the logical properties of the protocol.

 
Table 5:  The wide-mouthed-frog protocol

Since B trusts S, which says that A conveyed , B trusts A's jurisdiction over the generation of such keys, and B knows that the last message is `fresh' (it contains ), B can believe .

In the BAN-logic, the participants should be able to recognize and ignore its own messages. There are two possibilities:

• either every participant stores every message sent in a database and checks every message received whether or not it is included in that database,
• or, every participant makes sure that he can recognize that a received message could not possibly originate from him.

In the non-idealized protocol description, it is clear that the second possibility is true. S never sends messages of the form where . However, messages received always have that format! If a programmer modified the message sent by S into , because he could reuse a procedure used by participant A, then the implicit assumption that every participant can recognize its own messages is no longer true. Hence, the formal proof is not valid any more.