Editing Burrows–Abadi–Needham logic (section)

== BAN logic analysis of the Wide Mouth Frog protocol ==
A very simple protocol – the [[Wide Mouth Frog protocol]] – allows two agents, ''A'' and ''B'', to establish secure communications, using a trusted authentication server, S, and synchronized clocks all around. Using standard notation the protocol can be specified as follows:
: ''A'' → ''S'': ''A'', {{mset|''T''<sub>''A''</sub>, ''K''<sub>''AB''</sub>, ''B''}}<sub>''K''<sub>''AS''</sub></sub>
: ''S'' → ''B'': {{mset|''T''<sub>''S''</sub>, ''K''<sub>''AB''</sub>, A}}<sub>''K''<sub>''BS''</sub></sub>

Agents A and B are equipped with keys ''K''<sub>''AS''</sub> and ''K''<sub>''BS''</sub>, respectively, for communicating securely with S.  So we have assumptions:
: ''A'' believes key(''K''<sub>''AS''</sub>, ''A''↔''S'')
: ''S'' believes key(''K''<sub>''AS''</sub>, ''A''↔''S'')
: ''B'' believes key(''K''<sub>''BS''</sub>, ''B''↔''S'')
: ''S'' believes key(''K''<sub>''BS''</sub>, ''B''↔''S'')

Agent ''A'' wants to initiate a secure conversation with ''B''.  It therefore invents a key, ''K''<sub>''AB''</sub>, which it will use to communicate with ''B''.  ''A'' believes that this key is secure, since it made up the key itself:
: ''A'' believes {{nowrap|key(''K''<sub>''AB''</sub>, ''A''↔''B'')}}

''B'' is willing to accept this key, as long as it is sure that it came from ''A'':
: ''B'' believes (''A'' has jurisdiction over {{nowrap|key(''K'', ''A''↔''B'')}})

Moreover, ''B'' is willing to trust ''S'' to accurately relay keys from ''A'':
: ''B'' believes (''S'' has jurisdiction over (''A'' believes {{nowrap|key(''K'', ''A''↔''B'')}}))

That is, if ''B'' believes that ''S'' believes that ''A'' wants to use a particular key to communicate with ''B'', then ''B'' will trust ''S'' and believe it also.

The goal is to have
: ''B'' believes key(''K''<sub>''AB''</sub>, ''A''↔''B'')

''A'' reads the clock, obtaining the current time ''t'', and sends the following message:
: 1 ''A''→''S'':  {{mset|''t'', key(''K''<sub>''AB''</sub>, ''A''↔''B'')}}<sub>''K''<sub>''AS''</sub></sub>

That is, it sends its chosen session key and the current time to ''S'', encrypted with its private authentication server key ''K''<sub>''AS''</sub>.

Since ''S'' believes that {{nowrap|key(''K''<sub>''AS''</sub>, ''A''↔''S'')}}, and ''S'' sees {{nowrap|{{mset|''t'', key(''K''<sub>''AB''</sub>, ''A''↔''B'')}}<sub>''K''<sub>''AS''</sub></sub>}}, then ''S'' concludes that ''A'' actually said {{nowrap|{{mset|''t'', key(''K''<sub>''AB''</sub>, ''A''↔''B'')}}}}.  (In particular, ''S'' believes that the message was not manufactured out of whole cloth by some attacker.)

Since the clocks are synchronized, we can assume
: ''S'' believes fresh(''t'')

Since ''S'' believes fresh(''t'') and ''S'' believes ''A'' said {{nowrap|{{mset|''t'', key(''K''<sub>''AB''</sub>, ''A''↔''B'')}}}}, ''S'' believes that ''A'' actually ''believes'' that {{nowrap|key(''K''<sub>''AB''</sub>, ''A''↔''B'')}}.  (In particular, ''S'' believes that the message was not replayed by some attacker who captured it at some time in the past.)

''S'' then forwards the key to ''B'':
: 2 ''S''→''B'': {{mset|''t'', ''A'', ''A'' believes key(''K''<sub>''AB''</sub>, ''A''↔''B'')}}<sub>''K''<sub>''BS''</sub></sub>

Because message 2 is encrypted with ''K''<sub>''BS''</sub>, and ''B'' believes {{nowrap|key(''K''<sub>''BS''</sub>, ''B''↔''S'')}}, ''B'' now believes that ''S'' said {{nowrap|{{mset|''t'', ''A'', ''A'' believes key(''K''<sub>''AB''</sub>, ''A''↔''B'')}}}}. Because the clocks are synchronized, ''B'' believes fresh(''t''), and so fresh(''A'' believes {{nowrap|key(''K''<sub>''AB''</sub>, ''A''↔''B'')}}).  Because ''B'' believes that ''S''{{'}}s statement is fresh, ''B'' believes that ''S'' believes that (''A'' believes {{nowrap|key(''K''<sub>''AB''</sub>, ''A''↔''B'')}}).  Because ''B'' believes that ''S'' is authoritative about what ''A'' believes, ''B'' believes that (''A'' believes {{nowrap|key(''K''<sub>''AB''</sub>, ''A''↔''B'')}}).  Because ''B'' believes that ''A'' is authoritative about session keys between ''A'' and ''B'', ''B'' believes {{nowrap|key(''K''<sub>''AB''</sub>, ''A''↔''B'')}}.  ''B'' can now contact ''A'' directly, using ''K''<sub>''AB''</sub> as a secret session key.

Now let's suppose that we abandon the assumption that the clocks are synchronized.  In that case, ''S'' gets message 1 from ''A'' with {{nowrap|{{mset|''t'', key(''K''<sub>''AB''</sub>, ''A''↔''B'')}}}}, but it can no longer conclude that ''t'' is fresh.  It knows that ''A'' sent this message at ''some'' time in the past (because it is encrypted with ''K''<sub>''AS''</sub>) but not that this is a recent message, so ''S'' doesn't believe that ''A'' necessarily wants to continue to use the key ''K''<sub>''AB''</sub>.  This points directly at an attack on the protocol: An attacker who can capture messages can guess one of the old session keys ''K''<sub>''AB''</sub>.  (This might take a long time.)  The attacker then replays the old {{nowrap|{{mset|''t'', key(''K''<sub>''AB''</sub>, ''A''↔''B'')}}}} message, sending it to ''S''.  If the clocks aren't synchronized (perhaps as part of the same attack), ''S'' might believe this old message and request that ''B'' use the old, compromised key over again.

The original ''Logic of Authentication'' paper (linked below) contains this example and many others, including analyses of the [[Kerberos (protocol)|Kerberos]] handshake protocol, and two versions of the [[Andrew Project]] RPC handshake (one of which is defective).