--- a/src/HOL/Auth/Yahalom.thy Fri Sep 13 13:15:48 1996 +0200
+++ b/src/HOL/Auth/Yahalom.thy Fri Sep 13 13:16:57 1996 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Auth/OtwayRees
+(* Title: HOL/Auth/Yahalom
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
@@ -10,7 +10,7 @@
Proc. Royal Soc. 426 (1989)
*)
-OtwayRees = Shared +
+Yahalom = Shared +
consts yahalom :: "event list set"
inductive yahalom
@@ -26,13 +26,12 @@
(*Alice initiates a protocol run*)
YM1 "[| evs: yahalom; A ~= B |]
- ==> Says A B {|Nonce (newN evs), Agent A |} # evs : yahalom"
+ ==> Says A B {|Agent A, Nonce (newN evs)|} # evs : yahalom"
(*Bob's response to Alice's message. Bob doesn't know who
- the sender is, hence the A' in the sender field.
- We modify the published protocol by NOT encrypting NB.*)
+ the sender is, hence the A' in the sender field.*)
YM2 "[| evs: yahalom; B ~= Server;
- Says A' B {|Nonce NA, Agent A|} : set_of_list evs |]
+ Says A' B {|Agent A, Nonce NA|} : set_of_list evs |]
==> Says B Server
{|Agent B,
Crypt {|Agent A, Nonce NA, Nonce (newN evs)|} (shrK B)|}
@@ -40,34 +39,23 @@
(*The Server receives Bob's message. He responds by sending a
new session key to Alice, with a packet for forwarding to Bob.*)
- YM3 "[| evs: yahalom; B ~= Server;
+ YM3 "[| evs: yahalom; A ~= Server;
Says B' Server
- {|Nonce NA, Agent A, Agent B,
- Crypt {|Nonce NA, Agent A, Agent B|} (shrK A),
- Nonce NB,
- Crypt {|Nonce NA, Agent A, Agent B|} (shrK B)|}
+ {|Agent B, Crypt {|Agent A, Nonce NA, Nonce NB|} (shrK B)|}
: set_of_list evs |]
- ==> Says Server B
- {|Nonce NA,
- Crypt {|Nonce NA, Key (newK evs)|} (shrK A),
- Crypt {|Nonce NB, Key (newK evs)|} (shrK B)|}
+ ==> Says Server A
+ {|Crypt {|Agent B, Key (newK evs),
+ Nonce NA, Nonce NB|} (shrK A),
+ Crypt {|Agent A, Key (newK evs)|} (shrK B)|}
# evs : yahalom"
- (*Bob receives the Server's (?) message and compares the Nonces with
- those in the message he previously sent the Server.*)
+ (*Alice receives the Server's (?) message, checks her Nonce, and
+ uses the new session key to send Bob his Nonce.*)
YM4 "[| evs: yahalom; A ~= B;
- Says S B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|}
+ Says S A {|Crypt {|Agent B, Key K, Nonce NA, Nonce NB|} (shrK A),
+ X|}
: set_of_list evs;
- Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|}
- : set_of_list evs |]
- ==> (Says B A {|Nonce NA, X|}) # evs : yahalom"
-
- (*Alice checks her Nonce, then sends a dummy message to Bob,
- using the new session key.*)
- YM5 "[| evs: yahalom;
- Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|}
- : set_of_list evs;
- Says A B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |]
- ==> Says A B (Crypt (Agent A) K) # evs : yahalom"
+ Says A B {|Agent A, Nonce NA|} : set_of_list evs |]
+ ==> Says A B {|X, Crypt (Nonce NB) K|} # evs : yahalom"
end