--- a/src/HOL/Auth/Message.ML Fri Nov 29 17:58:18 1996 +0100
+++ b/src/HOL/Auth/Message.ML Fri Nov 29 18:03:21 1996 +0100
@@ -58,9 +58,8 @@
qed "keysFor_insert_MPair";
goalw thy [keysFor_def]
- "keysFor (insert (Crypt X K) H) = insert (invKey K) (keysFor H)";
+ "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)";
by (Auto_tac());
-by (Fast_tac 1);
qed "keysFor_insert_Crypt";
Addsimps [keysFor_empty, keysFor_Un, keysFor_UN,
@@ -68,7 +67,7 @@
keysFor_insert_Key, keysFor_insert_MPair,
keysFor_insert_Crypt];
-goalw thy [keysFor_def] "!!H. Crypt X K : H ==> invKey K : keysFor H";
+goalw thy [keysFor_def] "!!H. Crypt K X : H ==> invKey K : keysFor H";
by (Fast_tac 1);
qed "Crypt_imp_invKey_keysFor";
@@ -234,8 +233,8 @@
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
qed "parts_insert_Key";
-goal thy "parts (insert (Crypt X K) H) = \
-\ insert (Crypt X K) (parts (insert X H))";
+goal thy "parts (insert (Crypt K X) H) = \
+\ insert (Crypt K X) (parts (insert X H))";
by (rtac equalityI 1);
by (rtac subsetI 1);
by (etac parts.induct 1);
@@ -378,8 +377,8 @@
(*Can pull out enCrypted message if the Key is not known*)
goal thy "!!H. Key (invKey K) ~: analz H ==> \
-\ analz (insert (Crypt X K) H) = \
-\ insert (Crypt X K) (analz H)";
+\ analz (insert (Crypt K X) H) = \
+\ insert (Crypt K X) (analz H)";
by (rtac (analz_insert RSN (2, equalityI)) 1);
by (rtac subsetI 1);
by (etac analz.induct 1);
@@ -387,16 +386,16 @@
qed "analz_insert_Crypt";
goal thy "!!H. Key (invKey K) : analz H ==> \
-\ analz (insert (Crypt X K) H) <= \
-\ insert (Crypt X K) (analz (insert X H))";
+\ analz (insert (Crypt K X) H) <= \
+\ insert (Crypt K X) (analz (insert X H))";
by (rtac subsetI 1);
by (eres_inst_tac [("za","x")] analz.induct 1);
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
val lemma1 = result();
goal thy "!!H. Key (invKey K) : analz H ==> \
-\ insert (Crypt X K) (analz (insert X H)) <= \
-\ analz (insert (Crypt X K) H)";
+\ insert (Crypt K X) (analz (insert X H)) <= \
+\ analz (insert (Crypt K X) H)";
by (Auto_tac());
by (eres_inst_tac [("za","x")] analz.induct 1);
by (Auto_tac());
@@ -405,19 +404,19 @@
val lemma2 = result();
goal thy "!!H. Key (invKey K) : analz H ==> \
-\ analz (insert (Crypt X K) H) = \
-\ insert (Crypt X K) (analz (insert X H))";
+\ analz (insert (Crypt K X) H) = \
+\ insert (Crypt K X) (analz (insert X H))";
by (REPEAT (ares_tac [equalityI, lemma1, lemma2] 1));
qed "analz_insert_Decrypt";
(*Case analysis: either the message is secure, or it is not!
Effective, but can cause subgoals to blow up!
Use with expand_if; apparently split_tac does not cope with patterns
- such as "analz (insert (Crypt X K) H)" *)
-goal thy "analz (insert (Crypt X K) H) = \
+ such as "analz (insert (Crypt K X) H)" *)
+goal thy "analz (insert (Crypt K X) H) = \
\ (if (Key (invKey K) : analz H) \
-\ then insert (Crypt X K) (analz (insert X H)) \
-\ else insert (Crypt X K) (analz H))";
+\ then insert (Crypt K X) (analz (insert X H)) \
+\ else insert (Crypt K X) (analz H))";
by (case_tac "Key (invKey K) : analz H " 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [analz_insert_Crypt,
analz_insert_Decrypt])));
@@ -428,8 +427,8 @@
analz_Crypt_if];
(*This rule supposes "for the sake of argument" that we have the key.*)
-goal thy "analz (insert (Crypt X K) H) <= \
-\ insert (Crypt X K) (analz (insert X H))";
+goal thy "analz (insert (Crypt K X) H) <= \
+\ insert (Crypt K X) (analz (insert X H))";
by (rtac subsetI 1);
by (etac analz.induct 1);
by (Auto_tac());
@@ -496,7 +495,7 @@
qed "analz_insert_cong";
(*If there are no pairs or encryptions then analz does nothing*)
-goal thy "!!H. [| ALL X Y. {|X,Y|} ~: H; ALL X K. Crypt X K ~: H |] ==> \
+goal thy "!!H. [| ALL X Y. {|X,Y|} ~: H; ALL X K. Crypt K X ~: H |] ==> \
\ analz H = H";
by (Step_tac 1);
by (etac analz.induct 1);
@@ -528,7 +527,7 @@
val Nonce_synth = mk_cases "Nonce n : synth H";
val Key_synth = mk_cases "Key K : synth H";
val MPair_synth = mk_cases "{|X,Y|} : synth H";
-val Crypt_synth = mk_cases "Crypt X K : synth H";
+val Crypt_synth = mk_cases "Crypt K X : synth H";
AddSEs [Nonce_synth, Key_synth, MPair_synth, Crypt_synth];
@@ -589,7 +588,7 @@
by (Fast_tac 1);
qed "Key_synth_eq";
-goal thy "!!K. Key K ~: H ==> (Crypt X K : synth H) = (Crypt X K: H)";
+goal thy "!!K. Key K ~: H ==> (Crypt K X : synth H) = (Crypt K X: H)";
by (Fast_tac 1);
qed "Crypt_synth_eq";
@@ -660,9 +659,9 @@
qed "Fake_parts_insert";
goal thy
- "!!H. [| Crypt Y K : parts (insert X H); X: synth (analz G); \
+ "!!H. [| Crypt K Y : parts (insert X H); X: synth (analz G); \
\ Key K ~: analz G |] \
-\ ==> Crypt Y K : parts G Un parts H";
+\ ==> Crypt K Y : parts G Un parts H";
by (dtac (impOfSubs Fake_parts_insert) 1);
by (assume_tac 1);
by (fast_tac (!claset addDs [impOfSubs analz_subset_parts]
@@ -699,7 +698,7 @@
AddIffs [MPair_synth_analz];
goal thy "!!K. [| Key K : analz H; Key (invKey K) : analz H |] \
-\ ==> (Crypt X K : synth (analz H)) = (X : synth (analz H))";
+\ ==> (Crypt K X : synth (analz H)) = (X : synth (analz H))";
by (Fast_tac 1);
qed "Crypt_synth_analz";
--- a/src/HOL/Auth/Message.thy Fri Nov 29 17:58:18 1996 +0100
+++ b/src/HOL/Auth/Message.thy Fri Nov 29 18:03:21 1996 +0100
@@ -28,10 +28,10 @@
isSymKey :: key=>bool
"isSymKey K == (invKey K = K)"
- (*We do not assume Crypt (Crypt X K) (invKey K) = X
- because Crypt is a constructor! We assume that encryption is injective,
+ (*We do not assume Crypt (invKey K) (Crypt K X) = X
+ because Crypt a is constructor! We assume that encryption is injective,
which is not true in the real world. The alternative is to take
- Crypt as an uninterpreted function symbol satisfying the equation
+ Crypt an as uninterpreted function symbol satisfying the equation
above. This seems to require moving to ZF and regarding msg as an
inductive definition instead of a datatype.*)
@@ -43,7 +43,7 @@
| Nonce nat
| Key key
| MPair msg msg
- | Crypt msg key
+ | Crypt key msg
(*Allows messages of the form {|A,B,NA|}, etc...*)
syntax
@@ -56,7 +56,7 @@
constdefs (*Keys useful to decrypt elements of a message set*)
keysFor :: msg set => key set
- "keysFor H == invKey `` {K. EX X. Crypt X K : H}"
+ "keysFor H == invKey `` {K. EX X. Crypt K X : H}"
(** Inductive definition of all "parts" of a message. **)
@@ -66,7 +66,7 @@
Inj "X: H ==> X: parts H"
Fst "{|X,Y|} : parts H ==> X : parts H"
Snd "{|X,Y|} : parts H ==> Y : parts H"
- Body "Crypt X K : parts H ==> X : parts H"
+ Body "Crypt K X : parts H ==> X : parts H"
(** Inductive definition of "analz" -- what can be broken down from a set of
@@ -79,7 +79,7 @@
Inj "X: H ==> X: analz H"
Fst "{|X,Y|} : analz H ==> X : analz H"
Snd "{|X,Y|} : analz H ==> Y : analz H"
- Decrypt "[| Crypt X K : analz H; Key(invKey K): analz H |] ==> X : analz H"
+ Decrypt "[| Crypt K X : analz H; Key(invKey K): analz H |] ==> X : analz H"
(** Inductive definition of "synth" -- what can be built up from a set of
@@ -92,6 +92,6 @@
Inj "X: H ==> X: synth H"
Agent "Agent agt : synth H"
MPair "[| X: synth H; Y: synth H |] ==> {|X,Y|} : synth H"
- Crypt "[| X: synth H; Key(K): H |] ==> Crypt X K : synth H"
+ Crypt "[| X: synth H; Key(K): H |] ==> Crypt K X : synth H"
end
--- a/src/HOL/Auth/NS_Shared.ML Fri Nov 29 17:58:18 1996 +0100
+++ b/src/HOL/Auth/NS_Shared.ML Fri Nov 29 18:03:21 1996 +0100
@@ -20,7 +20,7 @@
goal thy
"!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
\ ==> EX N K. EX evs: ns_shared lost. \
-\ Says A B (Crypt {|Nonce N, Nonce N|} K) : set_of_list evs";
+\ Says A B (Crypt K {|Nonce N, Nonce N|}) : set_of_list evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (ns_shared.Nil RS ns_shared.NS1 RS ns_shared.NS2 RS ns_shared.NS3 RS ns_shared.NS4 RS ns_shared.NS5) 2);
by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
@@ -50,14 +50,14 @@
AddSEs [not_Says_to_self RSN (2, rev_notE)];
(*For reasoning about the encrypted portion of message NS3*)
-goal thy "!!evs. Says S A (Crypt {|N, B, K, X|} KA) : set_of_list evs \
+goal thy "!!evs. Says S A (Crypt KA {|N, B, K, X|}) : set_of_list evs \
\ ==> X : parts (sees lost Spy evs)";
by (fast_tac (!claset addSEs partsEs
addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
qed "NS3_msg_in_parts_sees_Spy";
goal thy
- "!!evs. Says Server A (Crypt {|NA, B, K, X|} (shrK A)) : set_of_list evs \
+ "!!evs. Says Server A (Crypt (shrK A) {|NA, B, K, X|}) : set_of_list evs \
\ ==> K : parts (sees lost Spy evs)";
by (fast_tac (!claset addSEs partsEs
addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
@@ -188,11 +188,11 @@
(*Describes the form of K, X and K' when the Server sends this message.*)
goal thy
- "!!evs. [| Says Server A (Crypt {|N, Agent B, K, X|} K') : set_of_list evs; \
+ "!!evs. [| Says Server A (Crypt K' {|N, Agent B, K, X|}) : set_of_list evs; \
\ evs : ns_shared lost |] \
\ ==> (EX evt: ns_shared lost. \
\ K = Key(newK evt) & \
-\ X = (Crypt {|K, Agent A|} (shrK B)) & \
+\ X = (Crypt (shrK B) {|K, Agent A|}) & \
\ K' = shrK A)";
by (etac rev_mp 1);
by (etac ns_shared.induct 1);
@@ -202,13 +202,13 @@
(*If the encrypted message appears then it originated with the Server*)
goal thy
- "!!evs. [| Crypt {|NA, Agent B, Key K, X|} (shrK A) \
+ "!!evs. [| Crypt (shrK A) {|NA, Agent B, Key K, X|} \
\ : parts (sees lost Spy evs); \
\ A ~: lost; evs : ns_shared lost |] \
-\ ==> X = (Crypt {|Key K, Agent A|} (shrK B)) & \
+\ ==> X = (Crypt (shrK B) {|Key K, Agent A|}) & \
\ Says Server A \
-\ (Crypt {|NA, Agent B, Key K, \
-\ Crypt {|Key K, Agent A|} (shrK B)|} (shrK A)) \
+\ (Crypt (shrK A) {|NA, Agent B, Key K, \
+\ Crypt (shrK B) {|Key K, Agent A|}|}) \
\ : set_of_list evs";
by (etac rev_mp 1);
by (parts_induct_tac 1);
@@ -220,11 +220,11 @@
OR reduces it to the Fake case.
Use Says_Server_message_form if applicable.*)
goal thy
- "!!evs. [| Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) \
+ "!!evs. [| Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|}) \
\ : set_of_list evs; evs : ns_shared lost |] \
\ ==> (EX evt: ns_shared lost. K = newK evt & \
\ length evt < length evs & \
-\ X = (Crypt {|Key K, Agent A|} (shrK B))) \
+\ X = (Crypt (shrK B) {|Key K, Agent A|})) \
\ | X : analz (sees lost Spy evs)";
by (case_tac "A : lost" 1);
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
@@ -261,7 +261,7 @@
We require that agents should behave like this subsequently also.*)
goal thy
"!!evs. evs : ns_shared lost ==> \
-\ (Crypt X (newK evt)) : parts (sees lost Spy evs) & \
+\ (Crypt (newK evt) X) : parts (sees lost Spy evs) & \
\ Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
by (etac ns_shared.induct 1);
by parts_Fake_tac;
@@ -314,7 +314,7 @@
goal thy
"!!evs. evs : ns_shared lost ==> \
\ EX A' NA' B' X'. ALL A NA B X. \
-\ Says Server A (Crypt {|NA, Agent B, Key K, X|} (shrK A)) \
+\ Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) \
\ : set_of_list evs --> A=A' & NA=NA' & B=B' & X=X'";
by (etac ns_shared.induct 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
@@ -333,10 +333,10 @@
(*In messages of this form, the session key uniquely identifies the rest*)
goal thy
"!!evs. [| Says Server A \
-\ (Crypt {|NA, Agent B, Key K, X|} (shrK A)) \
+\ (Crypt (shrK A) {|NA, Agent B, Key K, X|}) \
\ : set_of_list evs; \
\ Says Server A' \
-\ (Crypt {|NA', Agent B', Key K, X'|} (shrK A')) \
+\ (Crypt (shrK A') {|NA', Agent B', Key K, X'|}) \
\ : set_of_list evs; \
\ evs : ns_shared lost |] ==> A=A' & NA=NA' & B=B' & X = X'";
by (dtac lemma 1);
@@ -354,8 +354,8 @@
"!!evs. [| A ~: lost; B ~: lost; \
\ evs : ns_shared lost; evt: ns_shared lost |] \
\ ==> Says Server A \
-\ (Crypt {|NA, Agent B, Key K, \
-\ Crypt {|Key K, Agent A|} (shrK B)|} (shrK A)) \
+\ (Crypt (shrK A) {|NA, Agent B, Key K, \
+\ Crypt (shrK B) {|Key K, Agent A|}|}) \
\ : set_of_list evs --> \
\ (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list evs) --> \
\ Key K ~: analz (sees lost Spy evs)";
@@ -393,7 +393,7 @@
(*Final version: Server's message in the most abstract form*)
goal thy
"!!evs. [| Says Server A \
-\ (Crypt {|NA, Agent B, K, X|} K') : set_of_list evs; \
+\ (Crypt K' {|NA, Agent B, K, X|}) : set_of_list evs; \
\ (ALL NB. Says A Spy {|NA, NB, K|} ~: set_of_list evs); \
\ A ~: lost; B ~: lost; evs : ns_shared lost \
\ |] ==> K ~: analz (sees lost Spy evs)";
@@ -405,7 +405,7 @@
goal thy
"!!evs. [| C ~: {A,B,Server}; \
\ Says Server A \
-\ (Crypt {|NA, Agent B, K, X|} K') : set_of_list evs; \
+\ (Crypt K' {|NA, Agent B, K, X|}) : set_of_list evs; \
\ (ALL NB. Says A Spy {|NA, NB, K|} ~: set_of_list evs); \
\ A ~: lost; B ~: lost; evs : ns_shared lost |] \
\ ==> K ~: analz (sees lost C evs)";
@@ -424,11 +424,11 @@
(*If the encrypted message appears then it originated with the Server*)
goal thy
- "!!evs. [| Crypt {|Key K, Agent A|} (shrK B) : parts (sees lost Spy evs); \
+ "!!evs. [| Crypt (shrK B) {|Key K, Agent A|} : parts (sees lost Spy evs); \
\ B ~: lost; evs : ns_shared lost |] \
\ ==> EX NA. Says Server A \
-\ (Crypt {|NA, Agent B, Key K, \
-\ Crypt {|Key K, Agent A|} (shrK B)|} (shrK A)) \
+\ (Crypt (shrK A) {|NA, Agent B, Key K, \
+\ Crypt (shrK B) {|Key K, Agent A|}|}) \
\ : set_of_list evs";
by (etac rev_mp 1);
by (etac ns_shared.induct 1);
@@ -444,10 +444,10 @@
goal thy
"!!evs. [| B ~: lost; evs : ns_shared lost |] \
\ ==> Key K ~: analz (sees lost Spy evs) --> \
-\ Says Server A (Crypt {|NA, Agent B, Key K, X|} (shrK A)) \
+\ Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) \
\ : set_of_list evs --> \
-\ Crypt (Nonce NB) K : parts (sees lost Spy evs) --> \
-\ Says B A (Crypt (Nonce NB) K) : set_of_list evs";
+\ Crypt K (Nonce NB) : parts (sees lost Spy evs) --> \
+\ Says B A (Crypt K (Nonce NB)) : set_of_list evs";
by (etac ns_shared.induct 1);
by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);
by parts_Fake_tac;
@@ -461,7 +461,7 @@
by (Fast_tac 2);
by (REPEAT_FIRST (rtac impI ORELSE' etac conjE ORELSE' hyp_subst_tac));
(*Contradiction from the assumption
- Crypt (Nonce NB) (newK evsa) : parts (sees lost Spy evsa) *)
+ Crypt (newK evsa) (Nonce NB) : parts (sees lost Spy evsa) *)
by (dtac Crypt_imp_invKey_keysFor 1);
(**LEVEL 10**)
by (Asm_full_simp_tac 1);
@@ -475,12 +475,12 @@
val lemma = result();
goal thy
- "!!evs. [| Crypt (Nonce NB) K : parts (sees lost Spy evs); \
-\ Says Server A (Crypt {|NA, Agent B, Key K, X|} (shrK A)) \
+ "!!evs. [| Crypt K (Nonce NB) : parts (sees lost Spy evs); \
+\ Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) \
\ : set_of_list evs; \
\ ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list evs; \
\ A ~: lost; B ~: lost; evs : ns_shared lost |] \
-\ ==> Says B A (Crypt (Nonce NB) K) : set_of_list evs";
+\ ==> Says B A (Crypt K (Nonce NB)) : set_of_list evs";
by (fast_tac (!claset addSIs [lemma RS mp RS mp RS mp]
addSEs [Spy_not_see_encrypted_key RSN (2, rev_notE)]) 1);
qed "A_trust_NS4";
--- a/src/HOL/Auth/NS_Shared.thy Fri Nov 29 17:58:18 1996 +0100
+++ b/src/HOL/Auth/NS_Shared.thy Fri Nov 29 18:03:21 1996 +0100
@@ -36,15 +36,15 @@
the sender field.*)
NS2 "[| evs: ns_shared lost; A ~= B; A ~= Server;
Says A' Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
- ==> Says Server A
- (Crypt {|Nonce NA, Agent B, Key (newK evs),
- (Crypt {|Key (newK evs), Agent A|} (shrK B))|}
- (shrK A)) # evs : ns_shared lost"
+ ==> Says Server A (Crypt (shrK A)
+ {|Nonce NA, Agent B, Key (newK evs),
+ (Crypt (shrK B) {|Key (newK evs), Agent A|})|})
+ # evs : ns_shared lost"
(*We can't assume S=Server. Agent A "remembers" her nonce.
Can inductively show A ~= Server*)
NS3 "[| evs: ns_shared lost; A ~= B;
- Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))
+ Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
: set_of_list evs;
Says A Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
==> Says A B X # evs : ns_shared lost"
@@ -52,8 +52,8 @@
(*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 lost; A ~= B;
- Says A' B (Crypt {|Key K, Agent A|} (shrK B)) : set_of_list evs |]
- ==> Says B A (Crypt (Nonce (newN evs)) K) # evs : ns_shared lost"
+ Says A' B (Crypt (shrK B) {|Key K, Agent A|}) : set_of_list evs |]
+ ==> Says B A (Crypt K (Nonce (newN evs))) # evs : ns_shared lost"
(*Alice responds with Nonce NB if she has seen the key before.
Maybe should somehow check Nonce NA again.
@@ -61,17 +61,17 @@
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 lost; A ~= B;
- Says B' A (Crypt (Nonce NB) K) : set_of_list evs;
- Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))
+ Says B' A (Crypt K (Nonce NB)) : set_of_list evs;
+ Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
: set_of_list evs |]
- ==> Says A B (Crypt {|Nonce NB, Nonce NB|} K) # evs : ns_shared lost"
+ ==> Says A B (Crypt K {|Nonce NB, Nonce NB|}) # evs : ns_shared lost"
(*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 lost; A ~= Spy;
- Says B A (Crypt (Nonce NB) K) : set_of_list evs;
- Says Server A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))
+ Says B A (Crypt K (Nonce NB)) : set_of_list evs;
+ Says Server A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
: set_of_list evs |]
==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : ns_shared lost"
--- a/src/HOL/Auth/OtwayRees.ML Fri Nov 29 17:58:18 1996 +0100
+++ b/src/HOL/Auth/OtwayRees.ML Fri Nov 29 18:03:21 1996 +0100
@@ -23,7 +23,7 @@
goal thy
"!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
\ ==> EX K. EX NA. EX evs: otway lost. \
-\ Says B A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|} \
+\ Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
\ : set_of_list evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
@@ -65,7 +65,7 @@
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
qed "OR4_analz_sees_Spy";
-goal thy "!!evs. Says Server B {|NA, X, Crypt {|NB,K|} K'|} : set_of_list evs \
+goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set_of_list evs \
\ ==> K : parts (sees lost Spy evs)";
by (fast_tac (!claset addSEs partsEs
addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
@@ -137,7 +137,7 @@
\ Key (newK evs') ~: parts (sees lost Spy evs)";
by (parts_induct_tac 1);
by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
- addDs [impOfSubs analz_subset_parts,
+ addDs [impOfSubs analz_subset_parts,
impOfSubs parts_insert_subset_Un,
Suc_leD]
addss (!simpset))));
@@ -167,7 +167,7 @@
addSEs partsEs
addSDs [Says_imp_sees_Spy RS parts.Inj]
addEs [leD RS notE]
- addDs [impOfSubs analz_subset_parts,
+ addDs [impOfSubs analz_subset_parts,
impOfSubs parts_insert_subset_Un,
Suc_leD]
addss (!simpset))));
@@ -218,7 +218,7 @@
for Oops case.*)
goal thy
"!!evs. [| Says Server B \
-\ {|NA, X, Crypt {|NB, K|} (shrK B)|} : set_of_list evs; \
+\ {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs; \
\ evs : otway lost |] \
\ ==> (EX evt: otway lost. K = Key(newK evt)) & \
\ (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
@@ -284,7 +284,7 @@
goal thy
"!!evs. evs : otway lost ==> \
\ EX B' NA' NB' X'. ALL B NA NB X. \
-\ Says Server B {|NA, X, Crypt {|NB, K|} (shrK B)|} : set_of_list evs --> \
+\ Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs --> \
\ B=B' & NA=NA' & NB=NB' & X=X'";
by (etac otway.induct 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
@@ -301,9 +301,9 @@
val lemma = result();
goal thy
- "!!evs. [| Says Server B {|NA, X, Crypt {|NB, K|} (shrK B)|} \
+ "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} \
\ : set_of_list evs; \
-\ Says Server B' {|NA',X',Crypt {|NB',K|} (shrK B')|} \
+\ Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} \
\ : set_of_list evs; \
\ evs : otway lost |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
by (dtac lemma 1);
@@ -320,10 +320,10 @@
(*Only OR1 can have caused such a part of a message to appear.*)
goal thy
"!!evs. [| A ~: lost; evs : otway lost |] \
-\ ==> Crypt {|NA, Agent A, Agent B|} (shrK A) \
+\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \
\ : parts (sees lost Spy evs) --> \
\ Says A B {|NA, Agent A, Agent B, \
-\ Crypt {|NA, Agent A, Agent B|} (shrK A)|} \
+\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
\ : set_of_list evs";
by (parts_induct_tac 1);
qed_spec_mp "Crypt_imp_OR1";
@@ -334,7 +334,7 @@
goal thy
"!!evs. [| evs : otway lost; A ~: lost |] \
\ ==> EX B'. ALL B. \
-\ Crypt {|NA, Agent A, Agent B|} (shrK A) : parts (sees lost Spy evs) \
+\ Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (sees lost Spy evs) \
\ --> B = B'";
by (parts_induct_tac 1);
by (simp_tac (!simpset addsimps [all_conj_distrib]) 1);
@@ -345,8 +345,8 @@
val lemma = result();
goal thy
- "!!evs.[| Crypt {|NA, Agent A, Agent B|} (shrK A): parts(sees lost Spy evs); \
-\ Crypt {|NA, Agent A, Agent C|} (shrK A): parts(sees lost Spy evs); \
+ "!!evs.[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts(sees lost Spy evs); \
+\ Crypt (shrK A) {|NA, Agent A, Agent C|}: parts(sees lost Spy evs); \
\ evs : otway lost; A ~: lost |] \
\ ==> B = C";
by (dtac lemma 1);
@@ -365,9 +365,9 @@
over-simplified version of this protocol: see OtwayRees_Bad.*)
goal thy
"!!evs. [| A ~: lost; evs : otway lost |] \
-\ ==> Crypt {|NA, Agent A, Agent B|} (shrK A) \
+\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \
\ : parts (sees lost Spy evs) --> \
-\ Crypt {|NA', NA, Agent A', Agent A|} (shrK A) \
+\ Crypt (shrK A) {|NA', NA, Agent A', Agent A|} \
\ ~: parts (sees lost Spy evs)";
by (parts_induct_tac 1);
by (REPEAT (fast_tac (!claset addSEs (partsEs@[nonce_not_seen_now])
@@ -380,14 +380,14 @@
to start a run, then it originated with the Server!*)
goal thy
"!!evs. [| A ~: lost; A ~= Spy; evs : otway lost |] \
-\ ==> Crypt {|NA, Key K|} (shrK A) : parts (sees lost Spy evs) \
+\ ==> Crypt (shrK A) {|NA, Key K|} : parts (sees lost Spy evs) \
\ --> Says A B {|NA, Agent A, Agent B, \
-\ Crypt {|NA, Agent A, Agent B|} (shrK A)|} \
+\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
\ : set_of_list evs --> \
\ (EX NB. Says Server B \
\ {|NA, \
-\ Crypt {|NA, Key K|} (shrK A), \
-\ Crypt {|NB, Key K|} (shrK B)|} \
+\ Crypt (shrK A) {|NA, Key K|}, \
+\ Crypt (shrK B) {|NB, Key K|}|} \
\ : set_of_list evs)";
by (parts_induct_tac 1);
(*OR1: it cannot be a new Nonce, contradiction.*)
@@ -420,16 +420,16 @@
bad form of this protocol, even though we can prove
Spy_not_see_encrypted_key*)
goal thy
- "!!evs. [| Says B' A {|NA, Crypt {|NA, Key K|} (shrK A)|} \
+ "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} \
\ : set_of_list evs; \
\ Says A B {|NA, Agent A, Agent B, \
-\ Crypt {|NA, Agent A, Agent B|} (shrK A)|} \
+\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
\ : set_of_list evs; \
\ A ~: lost; A ~= Spy; evs : otway lost |] \
\ ==> EX NB. Says Server B \
\ {|NA, \
-\ Crypt {|NA, Key K|} (shrK A), \
-\ Crypt {|NB, Key K|} (shrK B)|} \
+\ Crypt (shrK A) {|NA, Key K|}, \
+\ Crypt (shrK B) {|NB, Key K|}|} \
\ : set_of_list evs";
by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
addEs partsEs
@@ -444,8 +444,8 @@
goal thy
"!!evs. [| A ~: lost; B ~: lost; evs : otway lost |] \
\ ==> Says Server B \
-\ {|NA, Crypt {|NA, Key K|} (shrK A), \
-\ Crypt {|NB, Key K|} (shrK B)|} : set_of_list evs --> \
+\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
+\ Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs --> \
\ Says B Spy {|NA, NB, Key K|} ~: set_of_list evs --> \
\ Key K ~: analz (sees lost Spy evs)";
by (etac otway.induct 1);
@@ -467,8 +467,8 @@
goal thy
"!!evs. [| Says Server B \
-\ {|NA, Crypt {|NA, K|} (shrK A), \
-\ Crypt {|NB, K|} (shrK B)|} : set_of_list evs; \
+\ {|NA, Crypt (shrK A) {|NA, K|}, \
+\ Crypt (shrK B) {|NB, K|}|} : set_of_list evs; \
\ Says B Spy {|NA, NB, K|} ~: set_of_list evs; \
\ A ~: lost; B ~: lost; evs : otway lost |] \
\ ==> K ~: analz (sees lost Spy evs)";
@@ -480,8 +480,8 @@
goal thy
"!!evs. [| C ~: {A,B,Server}; \
\ Says Server B \
-\ {|NA, Crypt {|NA, K|} (shrK A), \
-\ Crypt {|NB, K|} (shrK B)|} : set_of_list evs; \
+\ {|NA, Crypt (shrK A) {|NA, K|}, \
+\ Crypt (shrK B) {|NB, K|}|} : set_of_list evs; \
\ Says B Spy {|NA, NB, K|} ~: set_of_list evs; \
\ A ~: lost; B ~: lost; evs : otway lost |] \
\ ==> K ~: analz (sees lost C evs)";
@@ -498,11 +498,11 @@
know anything about X: it does NOT have to have the right form.*)
goal thy
"!!evs. [| B ~: lost; evs : otway lost |] \
-\ ==> Crypt {|NA, NB, Agent A, Agent B|} (shrK B) \
+\ ==> Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \
\ : parts (sees lost Spy evs) --> \
\ (EX X. Says B Server \
\ {|NA, Agent A, Agent B, X, \
-\ Crypt {|NA, NB, Agent A, Agent B|} (shrK B)|} \
+\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \
\ : set_of_list evs)";
by (parts_induct_tac 1);
by (auto_tac (!claset, !simpset addcongs [conj_cong]));
@@ -514,7 +514,7 @@
goal thy
"!!evs. [| evs : otway lost; B ~: lost |] \
\ ==> EX NA' A'. ALL NA A. \
-\ Crypt {|NA, NB, Agent A, Agent B|} (shrK B) : parts(sees lost Spy evs) \
+\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(sees lost Spy evs) \
\ --> NA = NA' & A = A'";
by (parts_induct_tac 1);
by (simp_tac (!simpset addsimps [all_conj_distrib]) 1);
@@ -524,9 +524,9 @@
val lemma = result();
goal thy
- "!!evs.[| Crypt {|NA, NB, Agent A, Agent B|} (shrK B) \
+ "!!evs.[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \
\ : parts(sees lost Spy evs); \
-\ Crypt {|NC, NB, Agent C, Agent B|} (shrK B) \
+\ Crypt (shrK B) {|NC, NB, Agent C, Agent B|} \
\ : parts(sees lost Spy evs); \
\ evs : otway lost; B ~: lost |] \
\ ==> NC = NA & C = A";
@@ -543,14 +543,14 @@
then it originated with the Server!*)
goal thy
"!!evs. [| B ~: lost; B ~= Spy; evs : otway lost |] \
-\ ==> Crypt {|NB, Key K|} (shrK B) : parts (sees lost Spy evs) \
+\ ==> Crypt (shrK B) {|NB, Key K|} : parts (sees lost Spy evs) \
\ --> (ALL X'. Says B Server \
\ {|NA, Agent A, Agent B, X', \
-\ Crypt {|NA, NB, Agent A, Agent B|} (shrK B)|} \
+\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \
\ : set_of_list evs \
\ --> Says Server B \
-\ {|NA, Crypt {|NA, Key K|} (shrK A), \
-\ Crypt {|NB, Key K|} (shrK B)|} \
+\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
+\ Crypt (shrK B) {|NB, Key K|}|} \
\ : set_of_list evs)";
by (parts_induct_tac 1);
(*OR1: it cannot be a new Nonce, contradiction.*)
@@ -577,16 +577,15 @@
has sent the correct message.*)
goal thy
"!!evs. [| B ~: lost; B ~= Spy; evs : otway lost; \
-\ Says S B {|NA, X, Crypt {|NB, Key K|} (shrK B)|} \
+\ Says S B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \
\ : set_of_list evs; \
\ Says B Server {|NA, Agent A, Agent B, X', \
-\ Crypt {|NA, NB, Agent A, Agent B|} \
-\ (shrK B)|} \
+\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
\ : set_of_list evs |] \
\ ==> Says Server B \
\ {|NA, \
-\ Crypt {|NA, Key K|} (shrK A), \
-\ Crypt {|NB, Key K|} (shrK B)|} \
+\ Crypt (shrK A) {|NA, Key K|}, \
+\ Crypt (shrK B) {|NB, Key K|}|} \
\ : set_of_list evs";
by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
addEs partsEs
@@ -600,15 +599,14 @@
goal thy
"!!evs. [| B ~: lost; evs : otway lost |] \
\ ==> Says Server B \
-\ {|NA, Crypt {|NA, Key K|} (shrK A), \
-\ Crypt {|NB, Key K|} (shrK B)|} : set_of_list evs --> \
+\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
+\ Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs --> \
\ (EX X. Says B Server {|NA, Agent A, Agent B, X, \
-\ Crypt {|NA, NB, Agent A, Agent B|} \
-\ (shrK B)|} \
+\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
\ : set_of_list evs)";
by (etac otway.induct 1);
by (Auto_tac());
-bd (Says_imp_sees_Spy RS parts.Inj) 1;
+by (dtac (Says_imp_sees_Spy RS parts.Inj) 1);
by (fast_tac (!claset addSEs [MPair_parts, Crypt_imp_OR2]) 1);
bind_thm ("OR3_imp_OR2", result() RSN (2,rev_mp) RS exE);
@@ -617,18 +615,15 @@
We could probably prove that X has the expected form, but that is not
strictly necessary for authentication.*)
goal thy
- "!!evs. [| Says B' A {|NA, Crypt {|NA, Key K|} (shrK A)|} \
+ "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} \
\ : set_of_list evs; \
\ Says A B {|NA, Agent A, Agent B, \
-\ Crypt {|NA, Agent A, Agent B|} (shrK A)|} \
+\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
\ : set_of_list evs; \
\ A ~: lost; A ~= Spy; B ~: lost; evs : otway lost |] \
\ ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X, \
-\ Crypt {|NA, NB, Agent A, Agent B|} \
-\ (shrK B)|} \
+\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |}\
\ : set_of_list evs";
by (fast_tac (!claset addSDs [A_trust_OR4]
- addSEs [OR3_imp_OR2]) 1);
+ addSEs [OR3_imp_OR2]) 1);
qed "A_auths_B";
-
-
--- a/src/HOL/Auth/OtwayRees.thy Fri Nov 29 17:58:18 1996 +0100
+++ b/src/HOL/Auth/OtwayRees.thy Fri Nov 29 18:03:21 1996 +0100
@@ -30,8 +30,8 @@
(*Alice initiates a protocol run*)
OR1 "[| evs: otway lost; A ~= B; B ~= Server |]
==> Says A B {|Nonce (newN evs), Agent A, Agent B,
- Crypt {|Nonce (newN evs), Agent A, Agent B|}
- (shrK A) |}
+ Crypt (shrK A)
+ {|Nonce (newN evs), Agent A, Agent B|} |}
# evs : otway lost"
(*Bob's response to Alice's message. Bob doesn't know who
@@ -41,8 +41,8 @@
Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |]
==> Says B Server
{|Nonce NA, Agent A, Agent B, X,
- Crypt {|Nonce NA, Nonce (newN evs),
- Agent A, Agent B|} (shrK B)|}
+ Crypt
+ (shrK B){|Nonce NA, Nonce (newN evs), Agent A, Agent B|}|}
# evs : otway lost"
(*The Server receives Bob's message and checks that the three NAs
@@ -51,30 +51,30 @@
OR3 "[| evs: otway lost; B ~= Server;
Says B' Server
{|Nonce NA, Agent A, Agent B,
- Crypt {|Nonce NA, Agent A, Agent B|} (shrK A),
- Crypt {|Nonce NA, Nonce NB, Agent A, Agent B|} (shrK B)|}
+ Crypt (shrK A) {|Nonce NA, Agent A, Agent B|},
+ Crypt (shrK B) {|Nonce NA, Nonce NB, Agent A, Agent 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)|}
+ Crypt (shrK A) {|Nonce NA, Key (newK evs)|},
+ Crypt (shrK B) {|Nonce NB, Key (newK evs)|}|}
# evs : otway lost"
(*Bob receives the Server's (?) message and compares the Nonces with
those in the message he previously sent the Server.*)
OR4 "[| evs: otway lost; A ~= B;
- Says S B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|}
+ Says S B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
: set_of_list evs;
Says B Server {|Nonce NA, Agent A, Agent B, X',
- Crypt {|Nonce NA, Nonce NB, Agent A, Agent B|}
- (shrK B)|}
+ Crypt (shrK B)
+ {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
: set_of_list evs |]
==> Says B A {|Nonce NA, X|} # evs : otway lost"
(*This message models possible leaks of session keys. The nonces
identify the protocol run.*)
Oops "[| evs: otway lost; B ~= Spy;
- Says Server B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|}
+ Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
: set_of_list evs |]
==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway lost"
--- a/src/HOL/Auth/OtwayRees_AN.ML Fri Nov 29 17:58:18 1996 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.ML Fri Nov 29 18:03:21 1996 +0100
@@ -22,7 +22,7 @@
goal thy
"!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
\ ==> EX K. EX NA. EX evs: otway lost. \
-\ Says B A (Crypt {|Nonce NA, Agent A, Agent B, Key K|} (shrK A)) \
+\ Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \
\ : set_of_list evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
@@ -59,7 +59,7 @@
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
qed "OR4_analz_sees_Spy";
-goal thy "!!evs. Says Server B {|X, Crypt {|NB, a, Agent B, K|} K'|} \
+goal thy "!!evs. Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} \
\ : set_of_list evs ==> K : parts (sees lost Spy evs)";
by (fast_tac (!claset addSEs partsEs
addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
@@ -176,8 +176,8 @@
(*Describes the form of K and NA when the Server sends this message.*)
goal thy
"!!evs. [| Says Server B \
-\ {|Crypt {|NA, Agent A, Agent B, K|} (shrK A), \
-\ Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs; \
+\ {|Crypt (shrK A) {|NA, Agent A, Agent B, K|}, \
+\ Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs; \
\ evs : otway lost |] \
\ ==> (EX evt: otway lost. K = Key(newK evt)) & \
\ (EX i. NA = Nonce i) & \
@@ -246,8 +246,8 @@
"!!evs. evs : otway lost ==> \
\ EX A' B' NA' NB'. ALL A B NA NB. \
\ Says Server B \
-\ {|Crypt {|NA, Agent A, Agent B, K|} (shrK A), \
-\ Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs \
+\ {|Crypt (shrK A) {|NA, Agent A, Agent B, K|}, \
+\ Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs \
\ --> A=A' & B=B' & NA=NA' & NB=NB'";
by (etac otway.induct 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
@@ -266,12 +266,12 @@
goal thy
"!!evs. [| Says Server B \
-\ {|Crypt {|NA, Agent A, Agent B, K|} (shrK A), \
-\ Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} \
+\ {|Crypt (shrK A) {|NA, Agent A, Agent B, K|}, \
+\ Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} \
\ : set_of_list evs; \
\ Says Server B' \
-\ {|Crypt {|NA', Agent A', Agent B', K|} (shrK A'), \
-\ Crypt {|NB', Agent A', Agent B', K|} (shrK B')|} \
+\ {|Crypt (shrK A') {|NA', Agent A', Agent B', K|}, \
+\ Crypt (shrK B') {|NB', Agent A', Agent B', K|}|} \
\ : set_of_list evs; \
\ evs : otway lost |] \
\ ==> A=A' & B=B' & NA=NA' & NB=NB'";
@@ -289,11 +289,11 @@
(*If the encrypted message appears then it originated with the Server!*)
goal thy
"!!evs. [| A ~: lost; evs : otway lost |] \
-\ ==> Crypt {|NA, Agent A, Agent B, Key K|} (shrK A) \
+\ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|} \
\ : parts (sees lost Spy evs) \
\ --> (EX NB. Says Server B \
-\ {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A), \
-\ Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|} \
+\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
+\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
\ : set_of_list evs)";
by (parts_induct_tac 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
@@ -308,12 +308,12 @@
Spy_not_see_encrypted_key. (We can implicitly infer freshness of
the Server's message from its nonce NA.)*)
goal thy
- "!!evs. [| Says B' A (Crypt {|NA, Agent A, Agent B, Key K|} (shrK A)) \
+ "!!evs. [| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) \
\ : set_of_list evs; \
\ A ~: lost; evs : otway lost |] \
\ ==> EX NB. Says Server B \
-\ {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A), \
-\ Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|} \
+\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
+\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
\ : set_of_list evs";
by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
addEs partsEs
@@ -328,8 +328,8 @@
goal thy
"!!evs. [| A ~: lost; B ~: lost; evs : otway lost |] \
\ ==> Says Server B \
-\ {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A), \
-\ Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|} \
+\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
+\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
\ : set_of_list evs --> \
\ Says B Spy {|NA, NB, Key K|} ~: set_of_list evs --> \
\ Key K ~: analz (sees lost Spy evs)";
@@ -351,8 +351,8 @@
goal thy
"!!evs. [| Says Server B \
-\ {|Crypt {|NA, Agent A, Agent B, K|} (shrK A), \
-\ Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs;\
+\ {|Crypt (shrK A) {|NA, Agent A, Agent B, K|}, \
+\ Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs;\
\ Says B Spy {|NA, NB, K|} ~: set_of_list evs; \
\ A ~: lost; B ~: lost; evs : otway lost |] \
\ ==> K ~: analz (sees lost Spy evs)";
@@ -364,8 +364,8 @@
goal thy
"!!evs. [| C ~: {A,B,Server}; \
\ Says Server B \
-\ {|Crypt {|NA, Agent A, Agent B, K|} (shrK A), \
-\ Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs;\
+\ {|Crypt (shrK A) {|NA, Agent A, Agent B, K|}, \
+\ Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs;\
\ Says B Spy {|NA, NB, K|} ~: set_of_list evs; \
\ A ~: lost; B ~: lost; evs : otway lost |] \
\ ==> K ~: analz (sees lost C evs)";
@@ -381,11 +381,11 @@
(*If the encrypted message appears then it originated with the Server!*)
goal thy
"!!evs. [| B ~: lost; evs : otway lost |] \
-\ ==> Crypt {|NB, Agent A, Agent B, Key K|} (shrK B) \
+\ ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|} \
\ : parts (sees lost Spy evs) \
\ --> (EX NA. Says Server B \
-\ {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A), \
-\ Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|} \
+\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
+\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
\ : set_of_list evs)";
by (parts_induct_tac 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
@@ -398,11 +398,11 @@
has sent the correct message.*)
goal thy
"!!evs. [| B ~: lost; evs : otway lost; \
-\ Says S B {|X, Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|} \
+\ Says S B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
\ : set_of_list evs |] \
\ ==> EX NA. Says Server B \
-\ {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A), \
-\ Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|} \
+\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
+\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
\ : set_of_list evs";
by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
addEs partsEs
--- a/src/HOL/Auth/OtwayRees_AN.thy Fri Nov 29 17:58:18 1996 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.thy Fri Nov 29 18:03:21 1996 +0100
@@ -45,15 +45,15 @@
Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
: set_of_list evs |]
==> Says Server B
- {|Crypt {|Nonce NA, Agent A, Agent B, Key(newK evs)|} (shrK A),
- Crypt {|Nonce NB, Agent A, Agent B, Key(newK evs)|} (shrK B)|}
+ {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key(newK evs)|},
+ Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key(newK evs)|}|}
# evs : otway lost"
(*Bob receives the Server's (?) message and compares the Nonces with
those in the message he previously sent the Server.*)
OR4 "[| evs: otway lost; A ~= B;
Says S B {|X,
- Crypt {|Nonce NB, Agent A, Agent B, Key K|} (shrK B)|}
+ Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key K|}|}
: set_of_list evs;
Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
: set_of_list evs |]
@@ -63,8 +63,8 @@
identify the protocol run. B is not assumed to know shrK A.*)
Oops "[| evs: otway lost; B ~= Spy;
Says Server B
- {|Crypt {|Nonce NA, Agent A, Agent B, Key K|} (shrK A),
- Crypt {|Nonce NB, Agent A, Agent B, Key K|} (shrK B)|}
+ {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|},
+ Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key K|}|}
: set_of_list evs |]
==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway lost"
--- a/src/HOL/Auth/OtwayRees_Bad.ML Fri Nov 29 17:58:18 1996 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.ML Fri Nov 29 18:03:21 1996 +0100
@@ -25,7 +25,7 @@
goal thy
"!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
\ ==> EX K. EX NA. EX evs: otway. \
-\ Says B A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|} \
+\ Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
\ : set_of_list evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
@@ -68,7 +68,7 @@
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
qed "OR4_analz_sees_Spy";
-goal thy "!!evs. Says Server B {|NA, X, Crypt {|NB,K|} K'|} : set_of_list evs \
+goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set_of_list evs \
\ ==> K : parts (sees lost Spy evs)";
by (fast_tac (!claset addSEs partsEs
addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
@@ -218,7 +218,7 @@
for Oops case.*)
goal thy
"!!evs. [| Says Server B \
-\ {|NA, X, Crypt {|NB, K|} (shrK B)|} : set_of_list evs; \
+\ {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs; \
\ evs : otway |] \
\ ==> (EX evt: otway. K = Key(newK evt)) & \
\ (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
@@ -295,7 +295,7 @@
goal thy
"!!evs. evs : otway ==> \
\ EX B' NA' NB' X'. ALL B NA NB X. \
-\ Says Server B {|NA, X, Crypt {|NB, K|} (shrK B)|} : set_of_list evs --> \
+\ Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs --> \
\ B=B' & NA=NA' & NB=NB' & X=X'";
by (etac otway.induct 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
@@ -312,9 +312,9 @@
val lemma = result();
goal thy
- "!!evs. [| Says Server B {|NA, X, Crypt {|NB, K|} (shrK B)|} \
+ "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} \
\ : set_of_list evs; \
-\ Says Server B' {|NA',X',Crypt {|NB',K|} (shrK B')|} \
+\ Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} \
\ : set_of_list evs; \
\ evs : otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
by (dtac lemma 1);
@@ -329,8 +329,8 @@
goal thy
"!!evs. [| A ~: lost; B ~: lost; evs : otway |] \
\ ==> Says Server B \
-\ {|NA, Crypt {|NA, Key K|} (shrK A), \
-\ Crypt {|NB, Key K|} (shrK B)|} : set_of_list evs --> \
+\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
+\ Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs --> \
\ Says B Spy {|NA, NB, Key K|} ~: set_of_list evs --> \
\ Key K ~: analz (sees lost Spy evs)";
by (etac otway.induct 1);
@@ -353,8 +353,8 @@
goal thy
"!!evs. [| Says Server B \
-\ {|NA, Crypt {|NA, K|} (shrK A), \
-\ Crypt {|NB, K|} (shrK B)|} : set_of_list evs; \
+\ {|NA, Crypt (shrK A) {|NA, K|}, \
+\ Crypt (shrK B) {|NB, K|}|} : set_of_list evs; \
\ Says B Spy {|NA, NB, K|} ~: set_of_list evs; \
\ A ~: lost; B ~: lost; evs : otway |] \
\ ==> K ~: analz (sees lost Spy evs)";
@@ -371,10 +371,10 @@
this version.*)
goal thy
"!!evs. [| A ~: lost; A ~= B; evs : otway |] \
-\ ==> Crypt {|NA, Agent A, Agent B|} (shrK A) \
+\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \
\ : parts (sees lost Spy evs) --> \
\ Says A B {|NA, Agent A, Agent B, \
-\ Crypt {|NA, Agent A, Agent B|} (shrK A)|} \
+\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
\ : set_of_list evs";
by (parts_induct_tac 1);
by (Fast_tac 1);
@@ -387,14 +387,14 @@
substituting some other nonce NA' for NB.*)
goal thy
"!!evs. [| A ~: lost; A ~= Spy; evs : otway |] \
-\ ==> Crypt {|NA, Key K|} (shrK A) : parts (sees lost Spy evs) --> \
+\ ==> Crypt (shrK A) {|NA, Key K|} : parts (sees lost Spy evs) --> \
\ Says A B {|NA, Agent A, Agent B, \
-\ Crypt {|NA, Agent A, Agent B|} (shrK A)|} \
+\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
\ : set_of_list evs --> \
\ (EX B NB. Says Server B \
\ {|NA, \
-\ Crypt {|NA, Key K|} (shrK A), \
-\ Crypt {|NB, Key K|} (shrK B)|} \
+\ Crypt (shrK A) {|NA, Key K|}, \
+\ Crypt (shrK B) {|NB, Key K|}|} \
\ : set_of_list evs)";
by (parts_induct_tac 1);
(*OR1: it cannot be a new Nonce, contradiction.*)
@@ -415,12 +415,12 @@
in two different roles:
Says B' Server
{|Nonce NAa, Agent Aa, Agent A,
- Crypt {|Nonce NAa, Agent Aa, Agent A|} (shrK Aa), Nonce NA,
- Crypt {|Nonce NAa, Agent Aa, Agent A|} (shrK A)|}
+ Crypt (shrK Aa) {|Nonce NAa, Agent Aa, Agent A|}, Nonce NA,
+ Crypt (shrK A) {|Nonce NAa, Agent Aa, Agent A|}|}
: set_of_list evsa;
Says A B
{|Nonce NA, Agent A, Agent B,
- Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|}
+ Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}|}
: set_of_list evsa
*)
writeln "GIVE UP! on NA_Crypt_imp_Server_msg";
--- a/src/HOL/Auth/OtwayRees_Bad.thy Fri Nov 29 17:58:18 1996 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.thy Fri Nov 29 18:03:21 1996 +0100
@@ -29,8 +29,8 @@
(*Alice initiates a protocol run*)
OR1 "[| evs: otway; A ~= B; B ~= Server |]
==> Says A B {|Nonce (newN evs), Agent A, Agent B,
- Crypt {|Nonce (newN evs), Agent A, Agent B|}
- (shrK A) |}
+ Crypt (shrK A)
+ {|Nonce (newN evs), Agent A, Agent B|} |}
# evs : otway"
(*Bob's response to Alice's message. Bob doesn't know who
@@ -40,7 +40,7 @@
Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |]
==> Says B Server
{|Nonce NA, Agent A, Agent B, X, Nonce (newN evs),
- Crypt {|Nonce NA, Agent A, Agent B|} (shrK B)|}
+ Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
# evs : otway"
(*The Server receives Bob's message and checks that the three NAs
@@ -49,20 +49,20 @@
OR3 "[| evs: otway; B ~= Server;
Says B' Server
{|Nonce NA, Agent A, Agent B,
- Crypt {|Nonce NA, Agent A, Agent B|} (shrK A),
+ Crypt (shrK A) {|Nonce NA, Agent A, Agent B|},
Nonce NB,
- Crypt {|Nonce NA, Agent A, Agent B|} (shrK B)|}
+ Crypt (shrK B) {|Nonce NA, Agent A, Agent 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)|}
+ Crypt (shrK A) {|Nonce NA, Key (newK evs)|},
+ Crypt (shrK B) {|Nonce NB, Key (newK evs)|}|}
# evs : 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 S B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|}
+ Says S B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
: set_of_list evs;
Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|}
: set_of_list evs |]
@@ -71,7 +71,7 @@
(*This message models possible leaks of session keys. The nonces
identify the protocol run.*)
Oops "[| evs: otway; B ~= Spy;
- Says Server B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|}
+ Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
: set_of_list evs |]
==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway"
--- a/src/HOL/Auth/Shared.ML Fri Nov 29 17:58:18 1996 +0100
+++ b/src/HOL/Auth/Shared.ML Fri Nov 29 18:03:21 1996 +0100
@@ -120,7 +120,7 @@
AddSIs [sees_own_shrK, Spy_sees_lost];
(*Added for Yahalom/lost_tac*)
-goal thy "!!A. [| Crypt X (shrK A) : analz (sees lost Spy evs); A: lost |] \
+goal thy "!!A. [| Crypt (shrK A) X : analz (sees lost Spy evs); A: lost |] \
\ ==> X : analz (sees lost Spy evs)";
by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 1);
qed "Crypt_Spy_analz_lost";
@@ -172,14 +172,14 @@
qed_spec_mp "Says_imp_sees_Spy";
goal thy
- "!!evs. [| Says A B (Crypt X (shrK C)) : set_of_list evs; C : lost |] \
+ "!!evs. [| Says A B (Crypt (shrK C) X) : set_of_list evs; C : lost |] \
\ ==> X : analz (sees lost Spy evs)";
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
addss (!simpset)) 1);
qed "Says_Crypt_lost";
goal thy
- "!!evs. [| Says A B (Crypt X (shrK C)) : set_of_list evs; \
+ "!!evs. [| Says A B (Crypt (shrK C) X) : set_of_list evs; \
\ X ~: analz (sees lost Spy evs) |] \
\ ==> C ~: lost";
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
--- a/src/HOL/Auth/Yahalom.ML Fri Nov 29 17:58:18 1996 +0100
+++ b/src/HOL/Auth/Yahalom.ML Fri Nov 29 18:03:21 1996 +0100
@@ -22,7 +22,7 @@
goal thy
"!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
\ ==> EX X NB K. EX evs: yahalom lost. \
-\ Says A B {|X, Crypt (Nonce NB) K|} : set_of_list evs";
+\ Says A B {|X, Crypt K (Nonce NB)|} : set_of_list evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS yahalom.YM4) 2);
by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
@@ -54,7 +54,7 @@
(** For reasoning about the encrypted portion of messages **)
(*Lets us treat YM4 using a similar argument as for the Fake case.*)
-goal thy "!!evs. Says S A {|Crypt Y (shrK A), X|} : set_of_list evs ==> \
+goal thy "!!evs. Says S A {|Crypt (shrK A) Y, X|} : set_of_list evs ==> \
\ X : analz (sees lost Spy evs)";
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
qed "YM4_analz_sees_Spy";
@@ -63,7 +63,7 @@
YM4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
(*Relates to both YM4 and Oops*)
-goal thy "!!evs. Says S A {|Crypt {|B, K, NA, NB|} (shrK A), X|} \
+goal thy "!!evs. Says S A {|Crypt (shrK A) {|B, K, NA, NB|}, X|} \
\ : set_of_list evs ==> \
\ K : parts (sees lost Spy evs)";
by (fast_tac (!claset addSEs partsEs
@@ -145,7 +145,7 @@
(*Ready-made for the classical reasoner*)
-goal thy "!!evs. [| Says A B {|Crypt {|b, Key (newK evs), na, nb|} K, X|} \
+goal thy "!!evs. [| Says A B {|Crypt K {|b, Key (newK evs), na, nb|}, X|} \
\ : set_of_list evs; evs : yahalom lost |] \
\ ==> R";
by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
@@ -189,7 +189,7 @@
Oops as well as main secrecy property.*)
goal thy
"!!evs. [| Says Server A \
-\ {|Crypt {|Agent B, K, NA, NB|} (shrK A), X|} : set_of_list evs; \
+\ {|Crypt (shrK A) {|Agent B, K, NA, NB|}, X|} : set_of_list evs; \
\ evs : yahalom lost |] \
\ ==> (EX evt: yahalom lost. K = Key(newK evt))";
by (etac rev_mp 1);
@@ -222,7 +222,7 @@
We require that agents should behave like this subsequently also.*)
goal thy
"!!evs. evs : yahalom lost ==> \
-\ (Crypt X (newK evt)) : parts (sees lost Spy evs) & \
+\ (Crypt (newK evt) X) : parts (sees lost Spy evs) & \
\ Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
by (etac yahalom.induct 1);
by parts_Fake_tac;
@@ -273,7 +273,7 @@
"!!evs. evs : yahalom lost ==> \
\ EX A' B' NA' NB' X'. ALL A B NA NB X. \
\ Says Server A \
-\ {|Crypt {|Agent B, Key K, NA, NB|} (shrK A), X|} \
+\ {|Crypt (shrK A) {|Agent B, Key K, NA, NB|}, X|} \
\ : set_of_list evs --> A=A' & B=B' & NA=NA' & NB=NB' & X=X'";
by (etac yahalom.induct 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
@@ -289,10 +289,10 @@
goal thy
"!!evs. [| Says Server A \
-\ {|Crypt {|Agent B, Key K, NA, NB|} (shrK A), X|} \
+\ {|Crypt (shrK A) {|Agent B, Key K, NA, NB|}, X|} \
\ : set_of_list evs; \
\ Says Server A' \
-\ {|Crypt {|Agent B', Key K, NA', NB'|} (shrK A'), X'|} \
+\ {|Crypt (shrK A') {|Agent B', Key K, NA', NB'|}, X'|} \
\ : set_of_list evs; \
\ evs : yahalom lost |] \
\ ==> A=A' & B=B' & NA=NA' & NB=NB'";
@@ -306,12 +306,12 @@
(*If the encrypted message appears then it originated with the Server*)
goal thy
- "!!evs. [| Crypt {|Agent B, Key K, NA, NB|} (shrK A) \
+ "!!evs. [| Crypt (shrK A) {|Agent B, Key K, NA, NB|} \
\ : parts (sees lost Spy evs); \
\ A ~: lost; evs : yahalom lost |] \
\ ==> Says Server A \
-\ {|Crypt {|Agent B, Key K, NA, NB|} (shrK A), \
-\ Crypt {|Agent A, Key K|} (shrK B)|} \
+\ {|Crypt (shrK A) {|Agent B, Key K, NA, NB|}, \
+\ Crypt (shrK B) {|Agent A, Key K|}|} \
\ : set_of_list evs";
by (etac rev_mp 1);
by (parts_induct_tac 1);
@@ -323,8 +323,8 @@
goal thy
"!!evs. [| A ~: lost; B ~: lost; evs : yahalom lost |] \
\ ==> Says Server A \
-\ {|Crypt {|Agent B, Key K, NA, NB|} (shrK A), \
-\ Crypt {|Agent A, Key K|} (shrK B)|} \
+\ {|Crypt (shrK A) {|Agent B, Key K, NA, NB|}, \
+\ Crypt (shrK B) {|Agent A, Key K|}|} \
\ : set_of_list evs --> \
\ Says A Spy {|NA, NB, Key K|} ~: set_of_list evs --> \
\ Key K ~: analz (sees lost Spy evs)";
@@ -349,8 +349,8 @@
(*Final version: Server's message in the most abstract form*)
goal thy
"!!evs. [| Says Server A \
-\ {|Crypt {|Agent B, K, NA, NB|} (shrK A), \
-\ Crypt {|Agent A, K|} (shrK B)|} : set_of_list evs; \
+\ {|Crypt (shrK A) {|Agent B, K, NA, NB|}, \
+\ Crypt (shrK B) {|Agent A, K|}|} : set_of_list evs; \
\ Says A Spy {|NA, NB, K|} ~: set_of_list evs; \
\ A ~: lost; B ~: lost; evs : yahalom lost |] ==> \
\ K ~: analz (sees lost Spy evs)";
@@ -362,8 +362,8 @@
goal thy
"!!evs. [| C ~: {A,B,Server}; \
\ Says Server A \
-\ {|Crypt {|Agent B, K, NA, NB|} (shrK A), \
-\ Crypt {|Agent A, K|} (shrK B)|} : set_of_list evs; \
+\ {|Crypt (shrK A) {|Agent B, K, NA, NB|}, \
+\ Crypt (shrK B) {|Agent A, K|}|} : set_of_list evs; \
\ Says A Spy {|NA, NB, K|} ~: set_of_list evs; \
\ A ~: lost; B ~: lost; evs : yahalom lost |] ==> \
\ K ~: analz (sees lost C evs)";
@@ -379,12 +379,12 @@
(*B knows, by the first part of A's message, that the Server distributed
the key for A and B. But this part says nothing about nonces.*)
goal thy
- "!!evs. [| Crypt {|Agent A, Key K|} (shrK B) : parts (sees lost Spy evs); \
+ "!!evs. [| Crypt (shrK B) {|Agent A, Key K|} : parts (sees lost Spy evs); \
\ B ~: lost; evs : yahalom lost |] \
\ ==> EX NA NB. Says Server A \
-\ {|Crypt {|Agent B, Key K, \
-\ Nonce NA, Nonce NB|} (shrK A), \
-\ Crypt {|Agent A, Key K|} (shrK B)|} \
+\ {|Crypt (shrK A) {|Agent B, Key K, \
+\ Nonce NA, Nonce NB|}, \
+\ Crypt (shrK B) {|Agent A, Key K|}|} \
\ : set_of_list evs";
by (etac rev_mp 1);
by (parts_induct_tac 1);
@@ -429,7 +429,7 @@
goal thy
"!!evs. evs : yahalom lost ==> EX NA' A' B'. ALL NA A B. \
-\ Crypt {|Agent A, Nonce NA, NB|} (shrK B) : parts(sees lost Spy evs) \
+\ Crypt (shrK B) {|Agent A, Nonce NA, NB|} : parts(sees lost Spy evs) \
\ --> B ~: lost --> NA = NA' & A = A' & B = B'";
by (parts_induct_tac 1); (*100 seconds??*)
by (simp_tac (!simpset addsimps [all_conj_distrib]) 1);
@@ -439,9 +439,9 @@
val lemma = result();
goal thy
- "!!evs.[| Crypt {|Agent A, Nonce NA, NB|} (shrK B) \
+ "!!evs.[| Crypt (shrK B) {|Agent A, Nonce NA, NB|} \
\ : parts (sees lost Spy evs); \
-\ Crypt {|Agent A', Nonce NA', NB|} (shrK B') \
+\ Crypt (shrK B') {|Agent A', Nonce NA', NB|} \
\ : parts (sees lost Spy evs); \
\ evs : yahalom lost; B ~: lost; B' ~: lost |] \
\ ==> NA' = NA & A' = A & B' = B";
@@ -473,9 +473,9 @@
(*Variant useful for proving secrecy of NB*)
goal thy
- "!!evs.[| Says C D {|X, Crypt {|Agent A, Nonce NA, NB|} (shrK B)|} \
+ "!!evs.[| Says C D {|X, Crypt (shrK B) {|Agent A, Nonce NA, NB|}|} \
\ : set_of_list evs; B ~: lost; \
-\ Says C' D' {|X', Crypt {|Agent A', Nonce NA', NB|} (shrK B')|} \
+\ Says C' D' {|X', Crypt (shrK B') {|Agent A', Nonce NA', NB|}|} \
\ : set_of_list evs; \
\ NB ~: analz (sees lost Spy evs); \
\ evs : yahalom lost |] \
@@ -489,8 +489,8 @@
goal thy
"!!evs. [| B ~: lost; evs : yahalom lost |] \
\ ==> Nonce NB ~: analz (sees lost Spy evs) --> \
-\ Crypt {|Agent A, Nonce NA, Nonce NB|} (shrK B) : parts (sees lost Spy evs) \
-\ --> Crypt {|Agent A', Nonce NB, NB'|} (shrK B') ~: parts (sees lost Spy evs)";
+\ Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|} : parts (sees lost Spy evs) \
+\ --> Crypt (shrK B') {|Agent A', Nonce NB, NB'|} ~: parts (sees lost Spy evs)";
by (etac yahalom.induct 1);
by parts_Fake_tac;
by (REPEAT_FIRST
@@ -519,11 +519,11 @@
goal thy
"!!evs. evs : yahalom lost \
\ ==> Nonce NB ~: analz (sees lost Spy evs) --> \
-\ Crypt (Nonce NB) K : parts (sees lost Spy evs) --> \
+\ Crypt K (Nonce NB) : parts (sees lost Spy evs) --> \
\ (EX A B NA. Says Server A \
-\ {|Crypt {|Agent B, Key K, \
-\ Nonce NA, Nonce NB|} (shrK A), \
-\ Crypt {|Agent A, Key K|} (shrK B)|} \
+\ {|Crypt (shrK A) {|Agent B, Key K, \
+\ Nonce NA, Nonce NB|}, \
+\ Crypt (shrK B) {|Agent A, Key K|}|} \
\ : set_of_list evs)";
by (etac yahalom.induct 1);
by parts_Fake_tac;
@@ -552,11 +552,11 @@
goal thy
"!!evs. evs : yahalom lost \
\ ==> Key K ~: analz (sees lost Spy evs) --> \
-\ Crypt (Nonce NB) K : parts (sees lost Spy evs) --> \
+\ Crypt K (Nonce NB) : parts (sees lost Spy evs) --> \
\ (EX A B NA. Says Server A \
-\ {|Crypt {|Agent B, Key K, \
-\ Nonce NA, Nonce NB|} (shrK A), \
-\ Crypt {|Agent A, Key K|} (shrK B)|} \
+\ {|Crypt (shrK A) {|Agent B, Key K, \
+\ Nonce NA, Nonce NB|}, \
+\ Crypt (shrK B) {|Agent A, Key K|}|} \
\ : set_of_list evs)";
by (etac yahalom.induct 1);
by parts_Fake_tac;
@@ -580,10 +580,10 @@
(*YM3 can only be triggered by YM2*)
goal thy
"!!evs. [| Says Server A \
-\ {|Crypt {|Agent B, k, na, nb|} (shrK A), X|} : set_of_list evs; \
+\ {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} : set_of_list evs; \
\ evs : yahalom lost |] \
\ ==> EX B'. Says B' Server \
-\ {| Agent B, Crypt {|Agent A, na, nb|} (shrK B) |} \
+\ {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |} \
\ : set_of_list evs";
by (etac rev_mp 1);
by (etac yahalom.induct 1);
@@ -622,7 +622,7 @@
\ ALL E. Nonce NB : analz (Key``(newK``E) Un (sees lost Spy evs)) --> \
\ (EX K: newK``E. EX A B na X. \
\ Says Server A \
-\ {|Crypt {|Agent B, Key K, na, Nonce NB|} (shrK A), X|} \
+\ {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} \
\ : set_of_list evs) | Nonce NB : analz (sees lost Spy evs)";
by (etac yahalom.induct 1);
by analz_Fake_tac;
@@ -673,7 +673,7 @@
for the induction to carry through.*)
goal thy
"!!evs. [| Says Server A \
-\ {|Crypt {|Agent B, Key (newK evt), na, Nonce NB'|} (shrK A), X|} \
+\ {|Crypt (shrK A) {|Agent B, Key (newK evt), na, Nonce NB'|}, X|} \
\ : set_of_list evs; \
\ Nonce NB : analz (insert (Key (newK evt)) (sees lost Spy evs)); \
\ evs : yahalom lost |] \
@@ -688,7 +688,7 @@
goal thy
"!!evs. [| A ~: lost; B ~: lost; Spy: lost; evs : yahalom lost |] \
\ ==> Says B Server \
-\ {|Agent B, Crypt {|Agent A, Nonce NA, Nonce NB|} (shrK B)|} \
+\ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
\ : set_of_list evs --> \
\ (ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set_of_list evs) --> \
\ Nonce NB ~: analz (sees lost Spy evs)";
@@ -757,16 +757,16 @@
nonces are forced to agree with NA and NB). *)
goal thy
"!!evs. [| Says B Server \
-\ {|Agent B, Crypt {|Agent A, Nonce NA, Nonce NB|} (shrK B)|} \
+\ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
\ : set_of_list evs; \
-\ Says A' B {|Crypt {|Agent A, Key K|} (shrK B), \
-\ Crypt (Nonce NB) K|} : set_of_list evs; \
+\ Says A' B {|Crypt (shrK B) {|Agent A, Key K|}, \
+\ Crypt K (Nonce NB)|} : set_of_list evs; \
\ ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set_of_list evs; \
\ A ~: lost; B ~: lost; Spy: lost; evs : yahalom lost |] \
\ ==> Says Server A \
-\ {|Crypt {|Agent B, Key K, \
-\ Nonce NA, Nonce NB|} (shrK A), \
-\ Crypt {|Agent A, Key K|} (shrK B)|} \
+\ {|Crypt (shrK A) {|Agent B, Key K, \
+\ Nonce NA, Nonce NB|}, \
+\ Crypt (shrK B) {|Agent A, Key K|}|} \
\ : set_of_list evs";
by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1 THEN
--- a/src/HOL/Auth/Yahalom.thy Fri Nov 29 17:58:18 1996 +0100
+++ b/src/HOL/Auth/Yahalom.thy Fri Nov 29 18:03:21 1996 +0100
@@ -35,35 +35,35 @@
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)|}
+ Crypt (shrK B) {|Agent A, Nonce NA, Nonce (newN evs)|}|}
# evs : yahalom lost"
(*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 lost; A ~= Server;
Says B' Server
- {|Agent B, Crypt {|Agent A, Nonce NA, Nonce NB|} (shrK B)|}
+ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
: set_of_list evs |]
==> Says Server A
- {|Crypt {|Agent B, Key (newK evs),
- Nonce NA, Nonce NB|} (shrK A),
- Crypt {|Agent A, Key (newK evs)|} (shrK B)|}
+ {|Crypt (shrK A) {|Agent B, Key (newK evs),
+ Nonce NA, Nonce NB|},
+ Crypt (shrK B) {|Agent A, Key (newK evs)|}|}
# evs : yahalom lost"
(*Alice receives the Server's (?) message, checks her Nonce, and
uses the new session key to send Bob his Nonce.*)
YM4 "[| evs: yahalom lost; A ~= Server; A ~= B;
- Says S A {|Crypt {|Agent B, Key K, Nonce NA, Nonce NB|} (shrK A),
+ Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|},
X|} : set_of_list evs;
Says A B {|Agent A, Nonce NA|} : set_of_list evs |]
- ==> Says A B {|X, Crypt (Nonce NB) K|} # evs : yahalom lost"
+ ==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom lost"
(*This message models possible leaks of session keys. The Nonces
identify the protocol run. Quoting Server here ensures they are
correct.*)
Oops "[| evs: yahalom lost; A ~= Spy;
- Says Server A {|Crypt {|Agent B, Key K, Nonce NA, Nonce NB|}
- (shrK A),
+ Says Server A {|Crypt (shrK A)
+ {|Agent B, Key K, Nonce NA, Nonce NB|},
X|} : set_of_list evs |]
==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom lost"
--- a/src/HOL/Auth/Yahalom2.ML Fri Nov 29 17:58:18 1996 +0100
+++ b/src/HOL/Auth/Yahalom2.ML Fri Nov 29 18:03:21 1996 +0100
@@ -23,7 +23,7 @@
goal thy
"!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
\ ==> EX X NB K. EX evs: yahalom lost. \
-\ Says A B {|X, Crypt (Nonce NB) K|} : set_of_list evs";
+\ Says A B {|X, Crypt K (Nonce NB)|} : set_of_list evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS yahalom.YM4) 2);
by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
@@ -55,7 +55,7 @@
(** For reasoning about the encrypted portion of messages **)
(*Lets us treat YM4 using a similar argument as for the Fake case.*)
-goal thy "!!evs. Says S A {|NB, Crypt Y (shrK A), X|} : set_of_list evs ==> \
+goal thy "!!evs. Says S A {|NB, Crypt (shrK A) Y, X|} : set_of_list evs ==> \
\ X : analz (sees lost Spy evs)";
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
qed "YM4_analz_sees_Spy";
@@ -64,7 +64,7 @@
YM4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
(*Relates to both YM4 and Oops*)
-goal thy "!!evs. Says S A {|NB, Crypt {|B, K, NA|} (shrK A), X|} \
+goal thy "!!evs. Says S A {|NB, Crypt (shrK A) {|B, K, NA|}, X|} \
\ : set_of_list evs ==> \
\ K : parts (sees lost Spy evs)";
by (fast_tac (!claset addSEs partsEs
@@ -187,7 +187,7 @@
(*Describes the form of K when the Server sends this message. Useful for
Oops as well as main secrecy property.*)
goal thy
- "!!evs. [| Says Server A {|NB', Crypt {|Agent B, K, NA|} (shrK A), X|} \
+ "!!evs. [| Says Server A {|NB', Crypt (shrK A) {|Agent B, K, NA|}, X|} \
\ : set_of_list evs; \
\ evs : yahalom lost |] \
\ ==> (EX evt: yahalom lost. K = Key(newK evt)) & A ~= B";
@@ -251,7 +251,7 @@
"!!evs. evs : yahalom lost ==> \
\ EX A' B' NA' NB' X'. ALL A B NA NB X. \
\ Says Server A \
-\ {|NB, Crypt {|Agent B, Key K, NA|} (shrK A), X|} \
+\ {|NB, Crypt (shrK A) {|Agent B, Key K, NA|}, X|} \
\ : set_of_list evs --> A=A' & B=B' & NA=NA' & NB=NB' & X=X'";
by (etac yahalom.induct 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
@@ -267,10 +267,10 @@
goal thy
"!!evs. [| Says Server A \
-\ {|NB, Crypt {|Agent B, Key K, NA|} (shrK A), X|} \
+\ {|NB, Crypt (shrK A) {|Agent B, Key K, NA|}, X|} \
\ : set_of_list evs; \
\ Says Server A' \
-\ {|NB', Crypt {|Agent B', Key K, NA'|} (shrK A'), X'|} \
+\ {|NB', Crypt (shrK A') {|Agent B', Key K, NA'|}, X'|} \
\ : set_of_list evs; \
\ evs : yahalom lost |] \
\ ==> A=A' & B=B' & NA=NA' & NB=NB'";
@@ -288,8 +288,8 @@
"!!evs. [| A ~: lost; B ~: lost; A ~= B; \
\ evs : yahalom lost |] \
\ ==> Says Server A \
-\ {|NB, Crypt {|Agent B, Key K, NA|} (shrK A), \
-\ Crypt {|NB, Key K, Agent A|} (shrK B)|} \
+\ {|NB, Crypt (shrK A) {|Agent B, Key K, NA|}, \
+\ Crypt (shrK B) {|NB, Key K, Agent A|}|} \
\ : set_of_list evs --> \
\ Says A Spy {|NA, NB, Key K|} ~: set_of_list evs --> \
\ Key K ~: analz (sees lost Spy evs)";
@@ -316,8 +316,8 @@
(*Final version: Server's message in the most abstract form*)
goal thy
"!!evs. [| Says Server A \
-\ {|NB, Crypt {|Agent B, K, NA|} (shrK A), \
-\ Crypt {|NB, K, Agent A|} (shrK B)|} \
+\ {|NB, Crypt (shrK A) {|Agent B, K, NA|}, \
+\ Crypt (shrK B) {|NB, K, Agent A|}|} \
\ : set_of_list evs; \
\ Says A Spy {|NA, NB, K|} ~: set_of_list evs; \
\ A ~: lost; B ~: lost; evs : yahalom lost |] \
@@ -330,8 +330,8 @@
goal thy
"!!evs. [| C ~: {A,B,Server}; \
\ Says Server A \
-\ {|NB, Crypt {|Agent B, K, NA|} (shrK A), \
-\ Crypt {|NB, K, Agent A|} (shrK B)|} \
+\ {|NB, Crypt (shrK A) {|Agent B, K, NA|}, \
+\ Crypt (shrK B) {|NB, K, Agent A|}|} \
\ : set_of_list evs; \
\ Says A Spy {|NA, NB, K|} ~: set_of_list evs; \
\ A ~: lost; B ~: lost; evs : yahalom lost |] \
@@ -347,12 +347,12 @@
(*If the encrypted message appears then it originated with the Server.*)
goal thy
- "!!evs. [| Crypt {|Agent B, Key K, NA|} (shrK A) \
+ "!!evs. [| Crypt (shrK A) {|Agent B, Key K, NA|} \
\ : parts (sees lost Spy evs); \
\ A ~: lost; evs : yahalom lost |] \
\ ==> EX NB. Says Server A \
-\ {|NB, Crypt {|Agent B, Key K, NA|} (shrK A), \
-\ Crypt {|NB, Key K, Agent A|} (shrK B)|} \
+\ {|NB, Crypt (shrK A) {|Agent B, Key K, NA|}, \
+\ Crypt (shrK B) {|NB, Key K, Agent A|}|} \
\ : set_of_list evs";
by (etac rev_mp 1);
by (parts_induct_tac 1);
@@ -364,13 +364,13 @@
(*B knows, by the first part of A's message, that the Server distributed
the key for A and B. *)
goal thy
- "!!evs. [| Crypt {|Nonce NB, Key K, Agent A|} (shrK B) \
+ "!!evs. [| Crypt (shrK B) {|Nonce NB, Key K, Agent A|} \
\ : parts (sees lost Spy evs); \
\ B ~: lost; evs : yahalom lost |] \
\ ==> EX NA. Says Server A \
\ {|Nonce NB, \
-\ Crypt {|Agent B, Key K, Nonce NA|} (shrK A), \
-\ Crypt {|Nonce NB, Key K, Agent A|} (shrK B)|} \
+\ Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, \
+\ Crypt (shrK B) {|Nonce NB, Key K, Agent A|}|} \
\ : set_of_list evs";
by (etac rev_mp 1);
by (parts_induct_tac 1);
@@ -385,13 +385,13 @@
(*What can B deduce from receipt of YM4? Stronger and simpler than Yahalom
because we do not have to show that NB is secret. *)
goal thy
- "!!evs. [| Says A' B {|Crypt {|Nonce NB, Key K, Agent A|} (shrK B), \
-\ Crypt (Nonce NB) K|} : set_of_list evs; \
+ "!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|}, \
+\ Crypt K (Nonce NB)|} : set_of_list evs; \
\ A ~: lost; B ~: lost; evs : yahalom lost |] \
\ ==> EX NA. Says Server A \
\ {|Nonce NB, \
-\ Crypt {|Agent B, Key K, Nonce NA|} (shrK A), \
-\ Crypt {|Nonce NB, Key K, Agent A|} (shrK B)|} \
+\ Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, \
+\ Crypt (shrK B) {|Nonce NB, Key K, Agent A|}|} \
\ : set_of_list evs";
by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1);
by (fast_tac (!claset addSDs [B_trusts_YM4_shrK]) 1);
--- a/src/HOL/Auth/Yahalom2.thy Fri Nov 29 17:58:18 1996 +0100
+++ b/src/HOL/Auth/Yahalom2.thy Fri Nov 29 18:03:21 1996 +0100
@@ -48,25 +48,25 @@
: set_of_list evs |]
==> Says Server A
{|Nonce NB,
- Crypt {|Agent B, Key (newK evs), Nonce NA|} (shrK A),
- Crypt {|Nonce NB, Key (newK evs), Agent A|} (shrK B)|}
+ Crypt (shrK A) {|Agent B, Key (newK evs), Nonce NA|},
+ Crypt (shrK B) {|Nonce NB, Key (newK evs), Agent A|}|}
# evs : yahalom lost"
(*Alice receives the Server's (?) message, checks her Nonce, and
uses the new session key to send Bob his Nonce.*)
YM4 "[| evs: yahalom lost; A ~= Server; A ~= B;
- Says S A {|Nonce NB, Crypt {|Agent B, Key K, Nonce NA|} (shrK A),
+ 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 |]
- ==> Says A B {|X, Crypt (Nonce NB) K|} # evs : yahalom lost"
+ ==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom lost"
(*This message models possible leaks of session keys. The nonces
identify the protocol run. Quoting Server here ensures they are
correct. *)
Oops "[| evs: yahalom lost; A ~= Spy;
Says Server A {|Nonce NB,
- Crypt {|Agent B, Key K, Nonce NA|} (shrK A),
+ Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
X|} : set_of_list evs |]
==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom lost"