--- a/src/HOL/Auth/Yahalom2.thy Thu Jun 26 11:58:05 1997 +0200
+++ b/src/HOL/Auth/Yahalom2.thy Thu Jun 26 13:20:50 1997 +0200
@@ -35,7 +35,7 @@
(*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 lost; B ~= Server; Nonce NB ~: used evs;
- Says A' B {|Agent A, Nonce NA|} : set_of_list evs |]
+ Says A' B {|Agent A, Nonce NA|} : set evs |]
==> Says B Server
{|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
# evs : yahalom lost"
@@ -46,7 +46,7 @@
YM3 "[| evs: yahalom lost; A ~= B; A ~= Server; Key KAB ~: used evs;
Says B' Server {|Agent B, Nonce NB,
Crypt (shrK B) {|Agent A, Nonce NA|}|}
- : set_of_list evs |]
+ : set evs |]
==> Says Server A
{|Nonce NB,
Crypt (shrK A) {|Agent B, Key KAB, Nonce NA|},
@@ -58,8 +58,8 @@
YM4 "[| evs: yahalom lost; A ~= Server; A ~= B;
Says S A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
X|}
- : set_of_list evs;
- Says A B {|Agent A, Nonce NA|} : set_of_list evs |]
+ : set evs;
+ Says A B {|Agent A, Nonce NA|} : set evs |]
==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom lost"
(*This message models possible leaks of session keys. The nonces
@@ -68,7 +68,7 @@
Oops "[| evs: yahalom lost; A ~= Spy;
Says Server A {|Nonce NB,
Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
- X|} : set_of_list evs |]
+ X|} : set evs |]
==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom lost"
end