Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
--- a/src/HOL/Auth/NS_Public.thy Thu Sep 04 17:57:56 1997 +0200
+++ b/src/HOL/Auth/NS_Public.thy Fri Sep 05 12:24:13 1997 +0200
@@ -24,22 +24,22 @@
==> Says Spy B X # evs : ns_public"
(*Alice initiates a protocol run, sending a nonce to Bob*)
- NS1 "[| evs: ns_public; A ~= B; Nonce NA ~: used evs |]
+ NS1 "[| evs1: ns_public; A ~= B; Nonce NA ~: used evs1 |]
==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})
- # evs : ns_public"
+ # evs1 : ns_public"
(*Bob responds to Alice's message with a further nonce*)
- NS2 "[| evs: ns_public; A ~= B; Nonce NB ~: used evs;
- Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs |]
+ NS2 "[| evs2: ns_public; A ~= B; Nonce NB ~: used evs2;
+ Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs2 |]
==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})
- # evs : ns_public"
+ # evs2 : ns_public"
(*Alice proves her existence by sending NB back to Bob.*)
- NS3 "[| evs: ns_public;
- Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs;
+ NS3 "[| evs3: ns_public;
+ Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs3;
Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})
- : set evs |]
- ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs : ns_public"
+ : set evs3 |]
+ ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs3 : ns_public"
(**Oops message??**)
--- a/src/HOL/Auth/NS_Public_Bad.thy Thu Sep 04 17:57:56 1997 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.thy Fri Sep 05 12:24:13 1997 +0200
@@ -28,21 +28,21 @@
==> Says Spy B X # evs : ns_public"
(*Alice initiates a protocol run, sending a nonce to Bob*)
- NS1 "[| evs: ns_public; A ~= B; Nonce NA ~: used evs |]
+ NS1 "[| evs1: ns_public; A ~= B; Nonce NA ~: used evs1 |]
==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})
- # evs : ns_public"
+ # evs1 : ns_public"
(*Bob responds to Alice's message with a further nonce*)
- NS2 "[| evs: ns_public; A ~= B; Nonce NB ~: used evs;
- Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs |]
+ NS2 "[| evs2: ns_public; A ~= B; Nonce NB ~: used evs2;
+ Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs2 |]
==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|})
- # evs : ns_public"
+ # evs2 : ns_public"
(*Alice proves her existence by sending NB back to Bob.*)
- NS3 "[| evs: ns_public;
- Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs;
- Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs |]
- ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs : ns_public"
+ NS3 "[| evs3: ns_public;
+ Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs3;
+ Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs3 |]
+ ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs3 : ns_public"
(**Oops message??**)
--- a/src/HOL/Auth/NS_Shared.thy Thu Sep 04 17:57:56 1997 +0200
+++ b/src/HOL/Auth/NS_Shared.thy Fri Sep 05 12:24:13 1997 +0200
@@ -26,35 +26,35 @@
==> Says Spy B X # evs : ns_shared"
(*Alice initiates a protocol run, requesting to talk to any B*)
- NS1 "[| evs: ns_shared; A ~= Server; Nonce NA ~: used evs |]
- ==> Says A Server {|Agent A, Agent B, Nonce NA|} # evs
+ NS1 "[| evs1: ns_shared; A ~= Server; Nonce NA ~: used evs1 |]
+ ==> Says A Server {|Agent A, Agent B, Nonce NA|} # evs1
: ns_shared"
(*Server's response to Alice's message.
!! It may respond more than once to A's request !!
Server doesn't know who the true sender is, hence the A' in
the sender field.*)
- NS2 "[| evs: ns_shared; A ~= B; A ~= Server; Key KAB ~: used evs;
- Says A' Server {|Agent A, Agent B, Nonce NA|} : set evs |]
+ NS2 "[| evs2: ns_shared; A ~= B; A ~= Server; Key KAB ~: used evs2;
+ Says A' Server {|Agent A, Agent B, Nonce NA|} : set evs2 |]
==> Says Server A
(Crypt (shrK A)
{|Nonce NA, Agent B, Key KAB,
(Crypt (shrK B) {|Key KAB, Agent A|})|})
- # evs : ns_shared"
+ # evs2 : ns_shared"
(*We can't assume S=Server. Agent A "remembers" her nonce.
Can inductively show A ~= Server*)
- NS3 "[| evs: ns_shared; A ~= B;
+ NS3 "[| evs3: ns_shared; A ~= B;
Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
- : set evs;
- Says A Server {|Agent A, Agent B, Nonce NA|} : set evs |]
- ==> Says A B X # evs : ns_shared"
+ : set evs3;
+ Says A Server {|Agent A, Agent B, Nonce NA|} : set evs3 |]
+ ==> Says A B X # evs3 : ns_shared"
(*Bob's nonce exchange. He does not know who the message came
from, but responds to A because she is mentioned inside.*)
- NS4 "[| evs: ns_shared; A ~= B; Nonce NB ~: used evs;
- Says A' B (Crypt (shrK B) {|Key K, Agent A|}) : set evs |]
- ==> Says B A (Crypt K (Nonce NB)) # evs
+ NS4 "[| evs4: ns_shared; A ~= B; Nonce NB ~: used evs4;
+ Says A' B (Crypt (shrK B) {|Key K, Agent A|}) : set evs4 |]
+ ==> Says B A (Crypt K (Nonce NB)) # evs4
: ns_shared"
(*Alice responds with Nonce NB if she has seen the key before.
@@ -62,19 +62,19 @@
We do NOT send NB-1 or similar as the Spy cannot spoof such things.
Letting the Spy add or subtract 1 lets him send ALL nonces.
Instead we distinguish the messages by sending the nonce twice.*)
- NS5 "[| evs: ns_shared; A ~= B;
- Says B' A (Crypt K (Nonce NB)) : set evs;
+ NS5 "[| evs5: ns_shared; A ~= B;
+ Says B' A (Crypt K (Nonce NB)) : set evs5;
Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
- : set evs |]
- ==> Says A B (Crypt K {|Nonce NB, Nonce NB|}) # evs : ns_shared"
+ : set evs5 |]
+ ==> Says A B (Crypt K {|Nonce NB, Nonce NB|}) # evs5 : ns_shared"
(*This message models possible leaks of session keys.
The two Nonces identify the protocol run: the rule insists upon
the true senders in order to make them accurate.*)
- Oops "[| evs: ns_shared; A ~= Spy;
- Says B A (Crypt K (Nonce NB)) : set evs;
+ Oops "[| evso: ns_shared; A ~= Spy;
+ Says B A (Crypt K (Nonce NB)) : set evso;
Says Server A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
- : set evs |]
- ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : ns_shared"
+ : set evso |]
+ ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evso : ns_shared"
end
--- a/src/HOL/Auth/OtwayRees.thy Thu Sep 04 17:57:56 1997 +0200
+++ b/src/HOL/Auth/OtwayRees.thy Fri Sep 05 12:24:13 1997 +0200
@@ -28,53 +28,53 @@
==> Says Spy B X # evs : otway"
(*Alice initiates a protocol run*)
- OR1 "[| evs: otway; A ~= B; B ~= Server; Nonce NA ~: used evs |]
+ OR1 "[| evs1: otway; A ~= B; B ~= Server; Nonce NA ~: used evs1 |]
==> Says A B {|Nonce NA, Agent A, Agent B,
Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |}
- # evs : otway"
+ # evs1 : otway"
(*Bob's response to Alice's message. Bob doesn't know who
the sender is, hence the A' in the sender field.
Note that NB is encrypted.*)
- OR2 "[| evs: otway; B ~= Server; Nonce NB ~: used evs;
- Says A' B {|Nonce NA, Agent A, Agent B, X|} : set evs |]
+ OR2 "[| evs2: otway; B ~= Server; Nonce NB ~: used evs2;
+ Says A' B {|Nonce NA, Agent A, Agent B, X|} : set evs2 |]
==> Says B Server
{|Nonce NA, Agent A, Agent B, X,
Crypt (shrK B)
{|Nonce NA, Nonce NB, Agent A, Agent B|}|}
- # evs : otway"
+ # evs2 : otway"
(*The Server receives Bob's message and checks that the three NAs
match. Then he sends a new session key to Bob with a packet for
forwarding to Alice.*)
- OR3 "[| evs: otway; B ~= Server; Key KAB ~: used evs;
+ OR3 "[| evs3: otway; B ~= Server; Key KAB ~: used evs3;
Says B' Server
{|Nonce NA, Agent A, Agent B,
Crypt (shrK A) {|Nonce NA, Agent A, Agent B|},
Crypt (shrK B) {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
- : set evs |]
+ : set evs3 |]
==> Says Server B
{|Nonce NA,
Crypt (shrK A) {|Nonce NA, Key KAB|},
Crypt (shrK B) {|Nonce NB, Key KAB|}|}
- # evs : otway"
+ # evs3 : otway"
(*Bob receives the Server's (?) message and compares the Nonces with
those in the message he previously sent the Server.*)
- OR4 "[| evs: otway; A ~= B;
+ OR4 "[| evs4: otway; A ~= B;
Says B Server {|Nonce NA, Agent A, Agent B, X',
Crypt (shrK B)
{|Nonce NA, Nonce NB, Agent A, Agent B|}|}
- : set evs;
+ : set evs4;
Says S' B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
- : set evs |]
- ==> Says B A {|Nonce NA, X|} # evs : otway"
+ : set evs4 |]
+ ==> Says B A {|Nonce NA, X|} # evs4 : otway"
(*This message models possible leaks of session keys. The nonces
identify the protocol run.*)
- Oops "[| evs: otway; B ~= Spy;
+ Oops "[| evso: otway; B ~= Spy;
Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
- : set evs |]
- ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway"
+ : set evso |]
+ ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evso : otway"
end
--- a/src/HOL/Auth/OtwayRees_AN.thy Thu Sep 04 17:57:56 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.thy Fri Sep 05 12:24:13 1997 +0200
@@ -33,41 +33,41 @@
==> Says Spy B X # evs : otway"
(*Alice initiates a protocol run*)
- OR1 "[| evs: otway; A ~= B; B ~= Server |]
- ==> Says A B {|Agent A, Agent B, Nonce NA|} # evs : otway"
+ OR1 "[| evs1: otway; A ~= B; B ~= Server |]
+ ==> Says A B {|Agent A, Agent B, Nonce NA|} # evs1 : otway"
(*Bob's response to Alice's message. Bob doesn't know who
the sender is, hence the A' in the sender field.*)
- OR2 "[| evs: otway; B ~= Server;
- Says A' B {|Agent A, Agent B, Nonce NA|} : set evs |]
+ OR2 "[| evs2: otway; B ~= Server;
+ Says A' B {|Agent A, Agent B, Nonce NA|} : set evs2 |]
==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
- # evs : otway"
+ # evs2 : otway"
(*The Server receives Bob's message. Then he sends a new
session key to Bob with a packet for forwarding to Alice.*)
- OR3 "[| evs: otway; B ~= Server; A ~= B; Key KAB ~: used evs;
+ OR3 "[| evs3: otway; B ~= Server; A ~= B; Key KAB ~: used evs3;
Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
- : set evs |]
+ : set evs3 |]
==> Says Server B
{|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key KAB|},
Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key KAB|}|}
- # evs : otway"
+ # evs3 : otway"
(*Bob receives the Server's (?) message and compares the Nonces with
those in the message he previously sent the Server.*)
- OR4 "[| evs: otway; A ~= B;
- Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} : set evs;
+ OR4 "[| evs4: otway; A ~= B;
+ Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} : set evs4;
Says S' B {|X, Crypt(shrK B){|Nonce NB,Agent A,Agent B,Key K|}|}
- : set evs |]
- ==> Says B A X # evs : otway"
+ : set evs4 |]
+ ==> Says B A X # evs4 : otway"
(*This message models possible leaks of session keys. The nonces
identify the protocol run. B is not assumed to know shrK A.*)
- Oops "[| evs: otway; B ~= Spy;
+ Oops "[| evso: otway; B ~= Spy;
Says Server B
{|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|},
Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key K|}|}
- : set evs |]
- ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway"
+ : set evso |]
+ ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evso : otway"
end
--- a/src/HOL/Auth/OtwayRees_Bad.thy Thu Sep 04 17:57:56 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.thy Fri Sep 05 12:24:13 1997 +0200
@@ -26,51 +26,51 @@
==> Says Spy B X # evs : otway"
(*Alice initiates a protocol run*)
- OR1 "[| evs: otway; A ~= B; B ~= Server; Nonce NA ~: used evs |]
+ OR1 "[| evs1: otway; A ~= B; B ~= Server; Nonce NA ~: used evs1 |]
==> Says A B {|Nonce NA, Agent A, Agent B,
Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |}
- # evs : otway"
+ # evs1 : otway"
(*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.*)
- OR2 "[| evs: otway; B ~= Server; Nonce NB ~: used evs;
- Says A' B {|Nonce NA, Agent A, Agent B, X|} : set evs |]
+ OR2 "[| evs2: otway; B ~= Server; Nonce NB ~: used evs2;
+ Says A' B {|Nonce NA, Agent A, Agent B, X|} : set evs2 |]
==> Says B Server
{|Nonce NA, Agent A, Agent B, X, Nonce NB,
Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
- # evs : otway"
+ # evs2 : otway"
(*The Server receives Bob's message and checks that the three NAs
match. Then he sends a new session key to Bob with a packet for
forwarding to Alice.*)
- OR3 "[| evs: otway; B ~= Server; Key KAB ~: used evs;
+ OR3 "[| evs3: otway; B ~= Server; Key KAB ~: used evs3;
Says B' Server
{|Nonce NA, Agent A, Agent B,
Crypt (shrK A) {|Nonce NA, Agent A, Agent B|},
Nonce NB,
Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
- : set evs |]
+ : set evs3 |]
==> Says Server B
{|Nonce NA,
Crypt (shrK A) {|Nonce NA, Key KAB|},
Crypt (shrK B) {|Nonce NB, Key KAB|}|}
- # evs : otway"
+ # evs3 : otway"
(*Bob receives the Server's (?) message and compares the Nonces with
those in the message he previously sent the Server.*)
- OR4 "[| evs: otway; A ~= B;
+ OR4 "[| evs4: otway; A ~= B;
Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|}
- : set evs;
+ : set evs4;
Says S' B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
- : set evs |]
- ==> Says B A {|Nonce NA, X|} # evs : otway"
+ : set evs4 |]
+ ==> Says B A {|Nonce NA, X|} # evs4 : otway"
(*This message models possible leaks of session keys. The nonces
identify the protocol run.*)
- Oops "[| evs: otway; B ~= Spy;
+ Oops "[| evso: otway; B ~= Spy;
Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
- : set evs |]
- ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway"
+ : set evso |]
+ ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evso : otway"
end
--- a/src/HOL/Auth/Recur.thy Thu Sep 04 17:57:56 1997 +0200
+++ b/src/HOL/Auth/Recur.thy Fri Sep 05 12:24:13 1997 +0200
@@ -62,11 +62,11 @@
(*Alice initiates a protocol run.
"Agent Server" is just a placeholder, to terminate the nesting.*)
- RA1 "[| evs: recur; A ~= B; A ~= Server; Nonce NA ~: used evs |]
+ RA1 "[| evs1: recur; A ~= B; A ~= Server; Nonce NA ~: used evs1 |]
==> Says A B
(Hash[Key(shrK A)]
{|Agent A, Agent B, Nonce NA, Agent Server|})
- # evs : recur"
+ # evs1 : recur"
(*Bob's response to Alice's message. C might be the Server.
XA should be the Hash of the remaining components with KA, but
@@ -74,27 +74,27 @@
P is the previous recur message from Alice's caller.
NOTE: existing proofs don't need PA and are complicated by its
presence! See parts_Fake_tac.*)
- RA2 "[| evs: recur; B ~= C; B ~= Server; Nonce NB ~: used evs;
- Says A' B PA : set evs;
+ RA2 "[| evs2: recur; B ~= C; B ~= Server; Nonce NB ~: used evs2;
+ Says A' B PA : set evs2;
PA = {|XA, Agent A, Agent B, Nonce NA, P|} |]
==> Says B C (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|})
- # evs : recur"
+ # evs2 : recur"
(*The Server receives Bob's message and prepares a response.*)
- RA3 "[| evs: recur; B ~= Server;
- Says B' Server PB : set evs;
- (PB,RB,K) : respond evs |]
- ==> Says Server B RB # evs : recur"
+ RA3 "[| evs3: recur; B ~= Server;
+ Says B' Server PB : set evs3;
+ (PB,RB,K) : respond evs3 |]
+ ==> Says Server B RB # evs3 : recur"
(*Bob receives the returned message and compares the Nonces with
those in the message he previously sent the Server.*)
- RA4 "[| evs: recur; A ~= B;
+ RA4 "[| evs4: recur; A ~= B;
Says B C {|XH, Agent B, Agent C, Nonce NB,
- XA, Agent A, Agent B, Nonce NA, P|} : set evs;
+ XA, Agent A, Agent B, Nonce NA, P|} : set evs4;
Says C' B {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|},
Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
- RA|} : set evs |]
- ==> Says B A RA # evs : recur"
+ RA|} : set evs4 |]
+ ==> Says B A RA # evs4 : recur"
(**No "oops" message can easily be expressed. Each session key is
associated--in two separate messages--with two nonces.
--- a/src/HOL/Auth/WooLam.thy Thu Sep 04 17:57:56 1997 +0200
+++ b/src/HOL/Auth/WooLam.thy Fri Sep 05 12:24:13 1997 +0200
@@ -30,36 +30,36 @@
==> Says Spy B X # evs : woolam"
(*Alice initiates a protocol run*)
- WL1 "[| evs: woolam; A ~= B |]
- ==> Says A B (Agent A) # evs : woolam"
+ WL1 "[| evs1: woolam; A ~= B |]
+ ==> Says A B (Agent A) # evs1 : woolam"
(*Bob responds to Alice's message with a challenge.*)
- WL2 "[| evs: woolam; A ~= B;
- Says A' B (Agent A) : set evs |]
- ==> Says B A (Nonce NB) # evs : woolam"
+ WL2 "[| evs2: woolam; A ~= B;
+ Says A' B (Agent A) : set evs2 |]
+ ==> Says B A (Nonce NB) # evs2 : woolam"
(*Alice responds to Bob's challenge by encrypting NB with her key.
B is *not* properly determined -- Alice essentially broadcasts
her reply.*)
- WL3 "[| evs: woolam;
- Says A B (Agent A) : set evs;
- Says B' A (Nonce NB) : set evs |]
- ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs : woolam"
+ WL3 "[| evs3: woolam;
+ Says A B (Agent A) : set evs3;
+ Says B' A (Nonce NB) : set evs3 |]
+ ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs3 : woolam"
(*Bob forwards Alice's response to the Server. NOTE: usually
the messages are shown in chronological order, for clarity.
But here, exchanging the two events would cause the lemma
WL4_analz_sees_Spy to pick up the wrong assumption!*)
- WL4 "[| evs: woolam; B ~= Server;
- Says A' B X : set evs;
- Says A'' B (Agent A) : set evs |]
- ==> Says B Server {|Agent A, Agent B, X|} # evs : woolam"
+ WL4 "[| evs4: woolam; B ~= Server;
+ Says A' B X : set evs4;
+ Says A'' B (Agent A) : set evs4 |]
+ ==> Says B Server {|Agent A, Agent B, X|} # evs4 : woolam"
(*Server decrypts Alice's response for Bob.*)
- WL5 "[| evs: woolam; B ~= Server;
+ WL5 "[| evs5: woolam; B ~= Server;
Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|}
- : set evs |]
+ : set evs5 |]
==> Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|})
- # evs : woolam"
+ # evs5 : woolam"
end
--- a/src/HOL/Auth/Yahalom.thy Thu Sep 04 17:57:56 1997 +0200
+++ b/src/HOL/Auth/Yahalom.thy Fri Sep 05 12:24:13 1997 +0200
@@ -26,44 +26,44 @@
==> Says Spy B X # evs : yahalom"
(*Alice initiates a protocol run*)
- YM1 "[| evs: yahalom; A ~= B; Nonce NA ~: used evs |]
- ==> Says A B {|Agent A, Nonce NA|} # evs : yahalom"
+ YM1 "[| evs1: yahalom; A ~= B; Nonce NA ~: used evs1 |]
+ ==> Says A B {|Agent A, Nonce NA|} # evs1 : yahalom"
(*Bob's response to Alice's message. Bob doesn't know who
the sender is, hence the A' in the sender field.*)
- YM2 "[| evs: yahalom; B ~= Server; Nonce NB ~: used evs;
- Says A' B {|Agent A, Nonce NA|} : set evs |]
+ YM2 "[| evs2: yahalom; B ~= Server; Nonce NB ~: used evs2;
+ Says A' B {|Agent A, Nonce NA|} : set evs2 |]
==> Says B Server
{|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
- # evs : yahalom"
+ # evs2 : yahalom"
(*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; A ~= Server; Key KAB ~: used evs;
+ YM3 "[| evs3: yahalom; A ~= Server; Key KAB ~: used evs3;
Says B' Server
{|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
- : set evs |]
+ : set evs3 |]
==> Says Server A
{|Crypt (shrK A) {|Agent B, Key KAB, Nonce NA, Nonce NB|},
Crypt (shrK B) {|Agent A, Key KAB|}|}
- # evs : yahalom"
+ # evs3 : yahalom"
(*Alice receives the Server's (?) message, checks her Nonce, and
uses the new session key to send Bob his Nonce.*)
- YM4 "[| evs: yahalom; A ~= Server;
+ YM4 "[| evs4: yahalom; A ~= Server;
Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|},
- X|} : set evs;
- Says A B {|Agent A, Nonce NA|} : set evs |]
- ==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom"
+ X|} : set evs4;
+ Says A B {|Agent A, Nonce NA|} : set evs4 |]
+ ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 : yahalom"
(*This message models possible leaks of session keys. The Nonces
identify the protocol run. Quoting Server here ensures they are
correct.*)
- Oops "[| evs: yahalom; A ~= Spy;
+ Oops "[| evso: yahalom; A ~= Spy;
Says Server A {|Crypt (shrK A)
{|Agent B, Key K, Nonce NA, Nonce NB|},
- X|} : set evs |]
- ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom"
+ X|} : set evso |]
+ ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evso : yahalom"
constdefs
--- a/src/HOL/Auth/Yahalom2.thy Thu Sep 04 17:57:56 1997 +0200
+++ b/src/HOL/Auth/Yahalom2.thy Fri Sep 05 12:24:13 1997 +0200
@@ -29,45 +29,45 @@
==> Says Spy B X # evs : yahalom"
(*Alice initiates a protocol run*)
- YM1 "[| evs: yahalom; A ~= B; Nonce NA ~: used evs |]
- ==> Says A B {|Agent A, Nonce NA|} # evs : yahalom"
+ YM1 "[| evs1: yahalom; A ~= B; Nonce NA ~: used evs1 |]
+ ==> Says A B {|Agent A, Nonce NA|} # evs1 : yahalom"
(*Bob's response to Alice's message. Bob doesn't know who
the sender is, hence the A' in the sender field.*)
- YM2 "[| evs: yahalom; B ~= Server; Nonce NB ~: used evs;
- Says A' B {|Agent A, Nonce NA|} : set evs |]
+ YM2 "[| evs2: yahalom; B ~= Server; Nonce NB ~: used evs2;
+ Says A' B {|Agent A, Nonce NA|} : set evs2 |]
==> Says B Server
{|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
- # evs : yahalom"
+ # evs2 : yahalom"
(*The Server receives Bob's message. He responds by sending a
- new session key to Alice, with a packet for forwarding to Bob.
- !! Fields are reversed in the 2nd packet to prevent attacks!! *)
- YM3 "[| evs: yahalom; A ~= B; A ~= Server; Key KAB ~: used evs;
+ new session key to Alice, with a certificate for forwarding to Bob.
+ Fields are reversed in the 2nd certificate to prevent attacks!! *)
+ YM3 "[| evs3: yahalom; A ~= B; A ~= Server; Key KAB ~: used evs3;
Says B' Server {|Agent B, Nonce NB,
Crypt (shrK B) {|Agent A, Nonce NA|}|}
- : set evs |]
+ : set evs3 |]
==> Says Server A
{|Nonce NB,
Crypt (shrK A) {|Agent B, Key KAB, Nonce NA|},
Crypt (shrK B) {|Nonce NB, Key KAB, Agent A|}|}
- # evs : yahalom"
+ # evs3 : yahalom"
(*Alice receives the Server's (?) message, checks her Nonce, and
uses the new session key to send Bob his Nonce.*)
- YM4 "[| evs: yahalom; A ~= Server;
+ YM4 "[| evs4: yahalom; A ~= Server;
Says S A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
- X|} : set evs;
- Says A B {|Agent A, Nonce NA|} : set evs |]
- ==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom"
+ X|} : set evs4;
+ Says A B {|Agent A, Nonce NA|} : set evs4 |]
+ ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 : yahalom"
(*This message models possible leaks of session keys. The nonces
identify the protocol run. Quoting Server here ensures they are
correct. *)
- Oops "[| evs: yahalom; A ~= Spy;
+ Oops "[| evso: yahalom; A ~= Spy;
Says Server A {|Nonce NB,
Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
- X|} : set evs |]
- ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom"
+ X|} : set evso |]
+ ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evso : yahalom"
end