--- a/src/HOL/Auth/NS_Public.ML Thu Jun 26 13:20:50 1997 +0200
+++ b/src/HOL/Auth/NS_Public.ML Fri Jun 27 10:47:13 1997 +0200
@@ -134,7 +134,7 @@
(*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
goal thy
- "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs; \
+ "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs; \
\ A ~: lost; B ~: lost; evs : ns_public |] \
\ ==> Nonce NA ~: analz (sees lost Spy evs)";
by (etac rev_mp 1);
@@ -157,11 +157,11 @@
(*Authentication for A: if she receives message 2 and has used NA
to start a run, then B has sent message 2.*)
goal thy
- "!!evs. [| Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs;\
-\ Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
-\ : set evs;\
-\ A ~: lost; B ~: lost; evs : ns_public |] \
-\ ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
+ "!!evs. [| Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs; \
+\ Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
+\ : set evs; \
+\ A ~: lost; B ~: lost; evs : ns_public |] \
+\ ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
\ : set evs";
by (etac rev_mp 1);
(*prepare induction over Crypt (pubK A) {|NA,NB,B|} : parts H*)
@@ -237,7 +237,7 @@
(*Secrecy: Spy does not see the nonce sent in msg NS2 if A and B are secure*)
goal thy
"!!evs. [| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
-\ : set evs; \
+\ : set evs; \
\ A ~: lost; B ~: lost; evs : ns_public |] \
\ ==> Nonce NB ~: analz (sees lost Spy evs)";
by (etac rev_mp 1);
@@ -262,8 +262,8 @@
in message 2, then A has sent message 3.*)
goal thy
"!!evs. [| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
-\ : set evs; \
-\ Says A' B (Crypt (pubK B) (Nonce NB)): set evs; \
+\ : set evs; \
+\ Says A' B (Crypt (pubK B) (Nonce NB)): set evs; \
\ A ~: lost; B ~: lost; evs : ns_public |] \
\ ==> Says A B (Crypt (pubK B) (Nonce NB)) : set evs";
by (etac rev_mp 1);
@@ -294,8 +294,8 @@
NA, then A initiated the run using NA. SAME proof as B_trusts_NS3!*)
goal thy
"!!evs. [| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
-\ : set evs; \
-\ Says A' B (Crypt (pubK B) (Nonce NB)): set evs; \
+\ : set evs; \
+\ Says A' B (Crypt (pubK B) (Nonce NB)): set evs; \
\ A ~: lost; B ~: lost; evs : ns_public |] \
\ ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs";
by (etac rev_mp 1);
--- a/src/HOL/Auth/NS_Public.thy Thu Jun 26 13:20:50 1997 +0200
+++ b/src/HOL/Auth/NS_Public.thy Fri Jun 27 10:47:13 1997 +0200
@@ -31,8 +31,7 @@
(*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 |]
+ Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs |]
==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})
# evs : ns_public"
--- a/src/HOL/Auth/NS_Public_Bad.ML Thu Jun 26 13:20:50 1997 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.ML Fri Jun 27 10:47:13 1997 +0200
@@ -139,7 +139,7 @@
(*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
goal thy
- "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs; \
+ "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs; \
\ A ~: lost; B ~: lost; evs : ns_public |] \
\ ==> Nonce NA ~: analz (sees lost Spy evs)";
by (etac rev_mp 1);
@@ -162,9 +162,9 @@
(*Authentication for A: if she receives message 2 and has used NA
to start a run, then B has sent message 2.*)
goal thy
- "!!evs. [| Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs;\
-\ Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set evs;\
-\ A ~: lost; B ~: lost; evs : ns_public |] \
+ "!!evs. [| Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs; \
+\ Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set evs; \
+\ A ~: lost; B ~: lost; evs : ns_public |] \
\ ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set evs";
by (etac rev_mp 1);
(*prepare induction over Crypt (pubK A) {|NA,NB|} : parts H*)
@@ -240,9 +240,9 @@
(*NB remains secret PROVIDED Alice never responds with round 3*)
goal thy
- "!!evs.[| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs;\
-\ (ALL C. Says A C (Crypt (pubK C) (Nonce NB)) ~: set evs); \
-\ A ~: lost; B ~: lost; evs : ns_public |] \
+ "!!evs.[| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs; \
+\ (ALL C. Says A C (Crypt (pubK C) (Nonce NB)) ~: set evs); \
+\ A ~: lost; B ~: lost; evs : ns_public |] \
\ ==> Nonce NB ~: analz (sees lost Spy evs)";
by (etac rev_mp 1);
by (etac rev_mp 1);
@@ -270,8 +270,8 @@
in message 2, then A has sent message 3--to somebody....*)
goal thy
"!!evs. [| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) \
-\ : set evs; \
-\ Says A' B (Crypt (pubK B) (Nonce NB)): set evs; \
+\ : set evs; \
+\ Says A' B (Crypt (pubK B) (Nonce NB)): set evs; \
\ A ~: lost; B ~: lost; evs : ns_public |] \
\ ==> EX C. Says A C (Crypt (pubK C) (Nonce NB)) : set evs";
by (etac rev_mp 1);
@@ -294,7 +294,7 @@
(*Can we strengthen the secrecy theorem? NO*)
goal thy
- "!!evs. [| A ~: lost; B ~: lost; evs : ns_public |] \
+ "!!evs. [| A ~: lost; B ~: lost; evs : ns_public |] \
\ ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs \
\ --> Nonce NB ~: analz (sees lost Spy evs)";
by (analz_induct_tac 1);
--- a/src/HOL/Auth/NS_Shared.ML Thu Jun 26 13:20:50 1997 +0200
+++ b/src/HOL/Auth/NS_Shared.ML Fri Jun 27 10:47:13 1997 +0200
@@ -21,7 +21,7 @@
(*A "possibility property": there are traces that reach the end*)
goal thy
- "!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
+ "!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
\ ==> EX N K. EX evs: ns_shared lost. \
\ Says A B (Crypt K {|Nonce N, Nonce N|}) : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
@@ -38,7 +38,7 @@
by (rtac subsetI 1);
by (etac ns_shared.induct 1);
by (REPEAT_FIRST
- (blast_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
+ (blast_tac (!claset addIs (impOfSubs(sees_mono RS analz_mono RS synth_mono)
:: ns_shared.intrs))));
qed "ns_shared_mono";
@@ -128,7 +128,7 @@
(*Describes the form of K, X and K' when the Server sends this message.*)
goal thy
"!!evs. [| Says Server A (Crypt K' {|N, Agent B, Key K, X|}) \
-\ : set evs; \
+\ : set evs; \
\ evs : ns_shared lost |] \
\ ==> K ~: range shrK & \
\ X = (Crypt (shrK B) {|Key K, Agent A|}) & \
@@ -161,7 +161,7 @@
Use Says_Server_message_form if applicable.*)
goal thy
"!!evs. [| Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|}) \
-\ : set evs; evs : ns_shared lost |] \
+\ : set evs; evs : ns_shared lost |] \
\ ==> (K ~: range shrK & X = (Crypt (shrK B) {|Key K, Agent A|})) \
\ | X : analz (sees lost Spy evs)";
by (case_tac "A : lost" 1);
@@ -195,9 +195,9 @@
to encrypt messages containing other keys, in the actual protocol.
We require that agents should behave like this subsequently also.*)
goal thy
- "!!evs. [| evs : ns_shared lost; Kab ~: range shrK |] ==> \
-\ (Crypt KAB X) : parts (sees lost Spy evs) & \
-\ Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
+ "!!evs. [| evs : ns_shared lost; Kab ~: range shrK |] ==> \
+\ (Crypt KAB X) : parts (sees lost Spy evs) & \
+\ Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
by parts_induct_tac;
(*Deals with Faked messages*)
by (blast_tac (!claset addSEs partsEs
@@ -211,9 +211,9 @@
(*The equality makes the induction hypothesis easier to apply*)
goal thy
- "!!evs. evs : ns_shared lost ==> \
-\ ALL K KK. KK <= Compl (range shrK) --> \
-\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
+ "!!evs. evs : ns_shared lost ==> \
+\ ALL K KK. KK <= Compl (range shrK) --> \
+\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
\ (K : KK | Key K : analz (sees lost Spy evs))";
by (etac ns_shared.induct 1);
by analz_sees_tac;
@@ -242,7 +242,7 @@
"!!evs. evs : ns_shared lost ==> \
\ EX A' NA' B' X'. ALL A NA B X. \
\ Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) \
-\ : set evs --> A=A' & NA=NA' & B=B' & X=X'";
+\ : set 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])));
by (Step_tac 1);
@@ -260,10 +260,10 @@
goal thy
"!!evs. [| Says Server A \
\ (Crypt (shrK A) {|NA, Agent B, Key K, X|}) \
-\ : set evs; \
+\ : set evs; \
\ Says Server A' \
\ (Crypt (shrK A') {|NA', Agent B', Key K, X'|}) \
-\ : set evs; \
+\ : set evs; \
\ evs : ns_shared lost |] ==> A=A' & NA=NA' & B=B' & X = X'";
by (prove_unique_tac lemma 1);
qed "unique_session_keys";
@@ -276,8 +276,8 @@
\ ==> Says Server A \
\ (Crypt (shrK A) {|NA, Agent B, Key K, \
\ Crypt (shrK B) {|Key K, Agent A|}|}) \
-\ : set evs --> \
-\ (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs) --> \
+\ : set evs --> \
+\ (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs) --> \
\ Key K ~: analz (sees lost Spy evs)";
by (etac ns_shared.induct 1);
by analz_sees_tac;
@@ -308,8 +308,8 @@
(*Final version: Server's message in the most abstract form*)
goal thy
"!!evs. [| Says Server A \
-\ (Crypt K' {|NA, Agent B, Key K, X|}) : set evs; \
-\ (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs); \
+\ (Crypt K' {|NA, Agent B, Key K, X|}) : set evs; \
+\ (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs); \
\ A ~: lost; B ~: lost; evs : ns_shared lost \
\ |] ==> Key K ~: analz (sees lost Spy evs)";
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
@@ -320,8 +320,8 @@
goal thy
"!!evs. [| C ~: {A,B,Server}; \
\ Says Server A \
-\ (Crypt K' {|NA, Agent B, Key K, X|}) : set evs; \
-\ (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs); \
+\ (Crypt K' {|NA, Agent B, Key K, X|}) : set evs; \
+\ (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs); \
\ A ~: lost; B ~: lost; evs : ns_shared lost |] \
\ ==> Key K ~: analz (sees lost C evs)";
by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
@@ -354,11 +354,11 @@
goal thy
- "!!evs. [| B ~: lost; evs : ns_shared lost |] \
-\ ==> Key K ~: analz (sees lost Spy evs) --> \
+ "!!evs. [| B ~: lost; evs : ns_shared lost |] \
+\ ==> Key K ~: analz (sees lost Spy evs) --> \
\ Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) \
-\ : set evs --> \
-\ Crypt K (Nonce NB) : parts (sees lost Spy evs) --> \
+\ : set evs --> \
+\ Crypt K (Nonce NB) : parts (sees lost Spy evs) --> \
\ Says B A (Crypt K (Nonce NB)) : set evs";
by (etac ns_shared.induct 1);
by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);
@@ -390,8 +390,8 @@
goal thy
"!!evs. [| Crypt K (Nonce NB) : parts (sees lost Spy evs); \
\ Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) \
-\ : set evs; \
-\ ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs; \
+\ : set evs; \
+\ ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs; \
\ A ~: lost; B ~: lost; evs : ns_shared lost |] \
\ ==> Says B A (Crypt K (Nonce NB)) : set evs";
by (blast_tac (!claset addSIs [lemma RS mp RS mp RS mp]
--- a/src/HOL/Auth/OtwayRees.ML Thu Jun 26 13:20:50 1997 +0200
+++ b/src/HOL/Auth/OtwayRees.ML Fri Jun 27 10:47:13 1997 +0200
@@ -150,7 +150,7 @@
for Oops case.*)
goal thy
"!!evs. [| Says Server B \
-\ {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
+\ {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
\ evs : otway lost |] \
\ ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
by (etac rev_mp 1);
@@ -183,9 +183,9 @@
(*The equality makes the induction hypothesis easier to apply*)
goal thy
- "!!evs. evs : otway lost ==> \
-\ ALL K KK. KK <= Compl (range shrK) --> \
-\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
+ "!!evs. evs : otway lost ==> \
+\ ALL K KK. KK <= Compl (range shrK) --> \
+\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
\ (K : KK | Key K : analz (sees lost Spy evs))";
by (etac otway.induct 1);
by analz_sees_tac;
@@ -200,8 +200,8 @@
goal thy
- "!!evs. [| evs : otway lost; KAB ~: range shrK |] ==> \
-\ Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
+ "!!evs. [| evs : otway lost; KAB ~: range shrK |] ==> \
+\ Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
\ (K = KAB | Key K : analz (sees lost Spy evs))";
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
qed "analz_insert_freshK";
@@ -210,9 +210,9 @@
(*** The Key K uniquely identifies the Server's message. **)
goal thy
- "!!evs. evs : otway lost ==> \
-\ EX B' NA' NB' X'. ALL B NA NB X. \
-\ Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs --> \
+ "!!evs. evs : otway lost ==> \
+\ EX B' NA' NB' X'. ALL B NA NB X. \
+\ Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs --> \
\ B=B' & NA=NA' & NB=NB' & X=X'";
by (etac otway.induct 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
@@ -229,9 +229,9 @@
goal thy
"!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} \
-\ : set evs; \
+\ : set evs; \
\ Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} \
-\ : set evs; \
+\ : set evs; \
\ evs : otway lost |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
by (prove_unique_tac lemma 1);
qed "unique_session_keys";
@@ -257,7 +257,7 @@
goal thy
"!!evs. [| evs : otway lost; A ~: lost |] \
-\ ==> EX B'. ALL B. \
+\ ==> EX B'. ALL B. \
\ Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (sees lost Spy evs) \
\ --> B = B'";
by parts_induct_tac;
@@ -300,7 +300,7 @@
\ ==> Crypt (shrK A) {|NA, Key K|} : parts (sees lost Spy evs) \
\ --> Says A B {|NA, Agent A, Agent B, \
\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
-\ : set evs --> \
+\ : set evs --> \
\ (EX NB. Says Server B \
\ {|NA, \
\ Crypt (shrK A) {|NA, Key K|}, \
@@ -335,10 +335,10 @@
Spy_not_see_encrypted_key*)
goal thy
"!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} \
-\ : set evs; \
+\ : set evs; \
\ Says A B {|NA, Agent A, Agent B, \
\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
-\ : set evs; \
+\ : set evs; \
\ A ~: lost; A ~= Spy; evs : otway lost |] \
\ ==> EX NB. Says Server B \
\ {|NA, \
@@ -358,8 +358,8 @@
"!!evs. [| A ~: lost; B ~: lost; evs : otway lost |] \
\ ==> Says Server B \
\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
-\ Crypt (shrK B) {|NB, Key K|}|} : set evs --> \
-\ Says B Spy {|NA, NB, Key K|} ~: set evs --> \
+\ Crypt (shrK B) {|NB, Key K|}|} : set evs --> \
+\ Says B Spy {|NA, NB, Key K|} ~: set evs --> \
\ Key K ~: analz (sees lost Spy evs)";
by (etac otway.induct 1);
by analz_sees_tac;
@@ -382,8 +382,8 @@
goal thy
"!!evs. [| Says Server B \
\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
-\ Crypt (shrK B) {|NB, Key K|}|} : set evs; \
-\ Says B Spy {|NA, NB, Key K|} ~: set evs; \
+\ Crypt (shrK B) {|NB, Key K|}|} : set evs; \
+\ Says B Spy {|NA, NB, Key K|} ~: set evs; \
\ A ~: lost; B ~: lost; evs : otway lost |] \
\ ==> Key K ~: analz (sees lost Spy evs)";
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
@@ -395,8 +395,8 @@
"!!evs. [| C ~: {A,B,Server}; \
\ Says Server B \
\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
-\ Crypt (shrK B) {|NB, Key K|}|} : set evs; \
-\ Says B Spy {|NA, NB, Key K|} ~: set evs; \
+\ Crypt (shrK B) {|NB, Key K|}|} : set evs; \
+\ Says B Spy {|NA, NB, Key K|} ~: set evs; \
\ A ~: lost; B ~: lost; evs : otway lost |] \
\ ==> Key K ~: analz (sees lost C evs)";
by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
@@ -458,7 +458,7 @@
\ --> (ALL X'. Says B Server \
\ {|NA, Agent A, Agent B, X', \
\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \
-\ : set evs \
+\ : set evs \
\ --> Says Server B \
\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
\ Crypt (shrK B) {|NB, Key K|}|} \
@@ -486,10 +486,10 @@
goal thy
"!!evs. [| B ~: lost; B ~= Spy; evs : otway lost; \
\ Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \
-\ : set evs; \
+\ : set evs; \
\ Says B Server {|NA, Agent A, Agent B, X', \
\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
-\ : set evs |] \
+\ : set evs |] \
\ ==> Says Server B \
\ {|NA, \
\ Crypt (shrK A) {|NA, Key K|}, \
@@ -507,7 +507,7 @@
"!!evs. [| B ~: lost; evs : otway lost |] \
\ ==> Says Server B \
\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
-\ Crypt (shrK B) {|NB, Key K|}|} : set evs --> \
+\ Crypt (shrK B) {|NB, Key K|}|} : set evs --> \
\ (EX X. Says B Server {|NA, Agent A, Agent B, X, \
\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
\ : set evs)";
@@ -523,13 +523,11 @@
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 (shrK A) {|NA, Key K|}|} \
-\ : set evs; \
-\ Says A B {|NA, Agent A, Agent B, \
-\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
-\ : set evs; \
-\ A ~: lost; A ~= Spy; B ~: lost; evs : otway lost |] \
-\ ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X, \
+ "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
+\ Says A B {|NA, Agent A, Agent B, \
+\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
+\ A ~: lost; A ~= Spy; B ~: lost; evs : otway lost |] \
+\ ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X, \
\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |}\
\ : set evs";
by (blast_tac (!claset addSDs [A_trusts_OR4]
--- a/src/HOL/Auth/OtwayRees_AN.ML Thu Jun 26 13:20:50 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.ML Fri Jun 27 10:47:13 1997 +0200
@@ -139,7 +139,7 @@
"!!evs. [| Says Server B \
\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
-\ : set evs; \
+\ : set evs; \
\ evs : otway lost |] \
\ ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
by (etac rev_mp 1);
@@ -171,9 +171,9 @@
(*The equality makes the induction hypothesis easier to apply*)
goal thy
- "!!evs. evs : otway lost ==> \
-\ ALL K KK. KK <= Compl (range shrK) --> \
-\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
+ "!!evs. evs : otway lost ==> \
+\ ALL K KK. KK <= Compl (range shrK) --> \
+\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
\ (K : KK | Key K : analz (sees lost Spy evs))";
by (etac otway.induct 1);
by analz_sees_tac;
@@ -188,8 +188,8 @@
goal thy
- "!!evs. [| evs : otway lost; KAB ~: range shrK |] ==> \
-\ Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
+ "!!evs. [| evs : otway lost; KAB ~: range shrK |] ==> \
+\ Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
\ (K = KAB | Key K : analz (sees lost Spy evs))";
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
qed "analz_insert_freshK";
@@ -200,8 +200,8 @@
goal thy
"!!evs. evs : otway lost ==> \
\ EX A' B' NA' NB'. ALL A B NA NB. \
-\ Says Server B \
-\ {|Crypt (shrK A) {|NA, Agent A, Agent B, K|}, \
+\ Says Server B \
+\ {|Crypt (shrK A) {|NA, Agent A, Agent B, K|}, \
\ Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set evs \
\ --> A=A' & B=B' & NA=NA' & NB=NB'";
by (etac otway.induct 1);
@@ -222,11 +222,11 @@
"!!evs. [| Says Server B \
\ {|Crypt (shrK A) {|NA, Agent A, Agent B, K|}, \
\ Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} \
-\ : set evs; \
+\ : set evs; \
\ Says Server B' \
\ {|Crypt (shrK A') {|NA', Agent A', Agent B', K|}, \
\ Crypt (shrK B') {|NB', Agent A', Agent B', K|}|} \
-\ : set evs; \
+\ : set evs; \
\ evs : otway lost |] \
\ ==> A=A' & B=B' & NA=NA' & NB=NB'";
by (prove_unique_tac lemma 1);
@@ -257,7 +257,7 @@
Freshness may be inferred from nonce NA.*)
goal thy
"!!evs. [| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) \
-\ : set evs; \
+\ : set evs; \
\ A ~: lost; evs : otway lost |] \
\ ==> EX NB. Says Server B \
\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
@@ -277,8 +277,8 @@
\ ==> Says Server B \
\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
-\ : set evs --> \
-\ Says B Spy {|NA, NB, Key K|} ~: set evs --> \
+\ : set evs --> \
+\ Says B Spy {|NA, NB, Key K|} ~: set evs --> \
\ Key K ~: analz (sees lost Spy evs)";
by (etac otway.induct 1);
by analz_sees_tac;
@@ -302,8 +302,8 @@
"!!evs. [| Says Server B \
\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
-\ : set evs; \
-\ Says B Spy {|NA, NB, Key K|} ~: set evs; \
+\ : set evs; \
+\ Says B Spy {|NA, NB, Key K|} ~: set evs; \
\ A ~: lost; B ~: lost; evs : otway lost |] \
\ ==> Key K ~: analz (sees lost Spy evs)";
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
@@ -316,8 +316,8 @@
\ Says Server B \
\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
-\ : set evs; \
-\ Says B Spy {|NA, NB, Key K|} ~: set evs; \
+\ : set evs; \
+\ Says B Spy {|NA, NB, Key K|} ~: set evs; \
\ A ~: lost; B ~: lost; evs : otway lost |] \
\ ==> Key K ~: analz (sees lost C evs)";
by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
@@ -351,7 +351,7 @@
goal thy
"!!evs. [| B ~: lost; evs : otway lost; \
\ Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
-\ : set evs |] \
+\ : set evs |] \
\ ==> EX NA. Says Server B \
\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
--- a/src/HOL/Auth/OtwayRees_AN.thy Thu Jun 26 13:20:50 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.thy Fri Jun 27 10:47:13 1997 +0200
@@ -56,8 +56,7 @@
(*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 B Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
- : set evs;
+ Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} : set evs;
Says S' B {|X, Crypt(shrK B){|Nonce NB,Agent A,Agent B,Key K|}|}
: set evs |]
==> Says B A X # evs : otway lost"
--- a/src/HOL/Auth/OtwayRees_Bad.ML Thu Jun 26 13:20:50 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.ML Fri Jun 27 10:47:13 1997 +0200
@@ -140,7 +140,7 @@
for Oops case.*)
goal thy
"!!evs. [| Says Server B \
-\ {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
+\ {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
\ evs : otway |] \
\ ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
by (etac rev_mp 1);
@@ -172,9 +172,9 @@
(*The equality makes the induction hypothesis easier to apply*)
goal thy
- "!!evs. evs : otway ==> \
-\ ALL K KK. KK <= Compl (range shrK) --> \
-\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
+ "!!evs. evs : otway ==> \
+\ ALL K KK. KK <= Compl (range shrK) --> \
+\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
\ (K : KK | Key K : analz (sees lost Spy evs))";
by (etac otway.induct 1);
by analz_sees_tac;
@@ -199,9 +199,9 @@
(*** The Key K uniquely identifies the Server's message. **)
goal thy
- "!!evs. evs : otway ==> \
-\ EX B' NA' NB' X'. ALL B NA NB X. \
-\ Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs --> \
+ "!!evs. evs : otway ==> \
+\ EX B' NA' NB' X'. ALL B NA NB X. \
+\ Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs --> \
\ B=B' & NA=NA' & NB=NB' & X=X'";
by (etac otway.induct 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
@@ -217,10 +217,8 @@
val lemma = result();
goal thy
- "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} \
-\ : set evs; \
-\ Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} \
-\ : set evs; \
+ "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs; \
+\ Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} : set evs; \
\ evs : otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
by (prove_unique_tac lemma 1);
qed "unique_session_keys";
@@ -231,8 +229,8 @@
"!!evs. [| A ~: lost; B ~: lost; evs : otway |] \
\ ==> Says Server B \
\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
-\ Crypt (shrK B) {|NB, Key K|}|} : set evs --> \
-\ Says B Spy {|NA, NB, Key K|} ~: set evs --> \
+\ Crypt (shrK B) {|NB, Key K|}|} : set evs --> \
+\ Says B Spy {|NA, NB, Key K|} ~: set evs --> \
\ Key K ~: analz (sees lost Spy evs)";
by (etac otway.induct 1);
by analz_sees_tac;
@@ -253,10 +251,10 @@
val lemma = result() RS mp RS mp RSN(2,rev_notE);
goal thy
- "!!evs. [| Says Server B \
-\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
-\ Crypt (shrK B) {|NB, Key K|}|} : set evs; \
-\ Says B Spy {|NA, NB, Key K|} ~: set evs; \
+ "!!evs. [| Says Server B \
+\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
+\ Crypt (shrK B) {|NB, Key K|}|} : set evs; \
+\ Says B Spy {|NA, NB, Key K|} ~: set evs; \
\ A ~: lost; B ~: lost; evs : otway |] \
\ ==> Key K ~: analz (sees lost Spy evs)";
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
@@ -275,8 +273,7 @@
\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \
\ : parts (sees lost Spy evs) --> \
\ Says A B {|NA, Agent A, Agent B, \
-\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
-\ : set evs";
+\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs";
by parts_induct_tac;
by (Fake_parts_insert_tac 1);
by (Blast_tac 1);
@@ -288,16 +285,15 @@
(*Only it is FALSE. Somebody could make a fake message to Server
substituting some other nonce NA' for NB.*)
goal thy
- "!!evs. [| A ~: lost; A ~= Spy; evs : otway |] \
+ "!!evs. [| A ~: lost; A ~= Spy; evs : otway |] \
\ ==> Crypt (shrK A) {|NA, Key K|} : parts (sees lost Spy evs) --> \
-\ Says A B {|NA, Agent A, Agent B, \
+\ Says A B {|NA, Agent A, Agent B, \
\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
-\ : set evs --> \
+\ : set evs --> \
\ (EX B NB. Says Server B \
\ {|NA, \
\ Crypt (shrK A) {|NA, Key K|}, \
-\ Crypt (shrK B) {|NB, Key K|}|} \
-\ : set evs)";
+\ Crypt (shrK B) {|NB, Key K|}|} : set evs)";
by parts_induct_tac;
by (Fake_parts_insert_tac 1);
(*OR1: it cannot be a new Nonce, contradiction.*)
--- a/src/HOL/Auth/Recur.ML Thu Jun 26 13:20:50 1997 +0200
+++ b/src/HOL/Auth/Recur.ML Fri Jun 27 10:47:13 1997 +0200
@@ -21,11 +21,10 @@
(*Simplest case: Alice goes directly to the server*)
goal thy
- "!!A. A ~= Server \
+ "!!A. A ~= Server \
\ ==> EX K NA. EX evs: recur lost. \
\ Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, \
-\ Agent Server|} \
-\ : set evs";
+\ Agent Server|} : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (recur.Nil RS recur.RA1 RS
(respond.One RSN (4,recur.RA3))) 2);
@@ -38,8 +37,7 @@
"!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
\ ==> EX K. EX NA. EX evs: recur lost. \
\ Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
-\ Agent Server|} \
-\ : set evs";
+\ Agent Server|} : set evs";
by (cut_facts_tac [Nonce_supply2, Key_supply2] 1);
by (REPEAT (eresolve_tac [exE, conjE] 1));
by (REPEAT (resolve_tac [exI,bexI] 1));
@@ -58,8 +56,7 @@
"!!A B. [| A ~= B; B ~= C; A ~= Server; B ~= Server; C ~= Server |] \
\ ==> EX K. EX NA. EX evs: recur lost. \
\ Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
-\ Agent Server|} \
-\ : set evs";
+\ Agent Server|} : set evs";
by (cut_facts_tac [Nonce_supply3, Key_supply3] 1);
by (REPEAT (eresolve_tac [exE, conjE] 1));
by (REPEAT (resolve_tac [exI,bexI] 1));
@@ -82,7 +79,7 @@
by (rtac subsetI 1);
by (etac recur.induct 1);
by (REPEAT_FIRST
- (blast_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
+ (blast_tac (!claset addIs (impOfSubs(sees_mono RS analz_mono RS synth_mono)
:: recur.intrs))));
qed "recur_mono";
@@ -528,9 +525,8 @@
goalw thy [HPair_def]
"!!evs. [| Hash {|Key(shrK A), Agent A, Agent B, NA, P|} \
\ : parts (sees lost Spy evs); \
-\ A ~: lost; evs : recur lost |] \
-\ ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|}) \
-\ : set evs";
+\ A ~: lost; evs : recur lost |] \
+\ ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|}) : set evs";
by (etac rev_mp 1);
by parts_induct_tac;
by (Fake_parts_insert_tac 1);
@@ -547,7 +543,7 @@
goal thy
"!!evs. [| Crypt (shrK A) Y : parts (sees lost Spy evs); \
\ A ~: lost; A ~= Spy; evs : recur lost |] \
-\ ==> EX C RC. Says Server C RC : set evs & \
+\ ==> EX C RC. Says Server C RC : set evs & \
\ Crypt (shrK A) Y : parts {RC}";
by (etac rev_mp 1);
by parts_induct_tac;
--- a/src/HOL/Auth/Recur.thy Thu Jun 26 13:20:50 1997 +0200
+++ b/src/HOL/Auth/Recur.thy Fri Jun 27 10:47:13 1997 +0200
@@ -90,15 +90,13 @@
those in the message he previously sent the Server.*)
RA4 "[| evs: recur lost; 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 evs;
Says C' B {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|},
Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
- RA|}
- : set evs |]
+ RA|} : set evs |]
==> Says B A RA # evs : recur lost"
-(**No "oops" message can readily be expressed, since each session key is
+(**No "oops" message can easily be expressed. Each session key is
associated--in two separate messages--with two nonces.
***)
end
--- a/src/HOL/Auth/WooLam.ML Thu Jun 26 13:20:50 1997 +0200
+++ b/src/HOL/Auth/WooLam.ML Fri Jun 27 10:47:13 1997 +0200
@@ -21,8 +21,7 @@
goal thy
"!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
\ ==> EX NB. EX evs: woolam. \
-\ Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) \
-\ : set evs";
+\ Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (woolam.Nil RS woolam.WL1 RS woolam.WL2 RS woolam.WL3 RS
woolam.WL4 RS woolam.WL5) 2);
@@ -107,7 +106,7 @@
Alice, then she originated that certificate. But we DO NOT know that B
ever saw it: the Spy may have rerouted the message to the Server.*)
goal thy
- "!!evs. [| A ~: lost; evs : woolam; \
+ "!!evs. [| A ~: lost; evs : woolam; \
\ Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} \
\ : set evs |] \
\ ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
@@ -121,8 +120,8 @@
(*Server sent WL5 only if it received the right sort of message*)
goal thy
- "!!evs. evs : woolam ==> \
-\ Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs \
+ "!!evs. evs : woolam ==> \
+\ Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs \
\ --> (EX B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|} \
\ : set evs)";
by parts_induct_tac;
@@ -133,8 +132,8 @@
(*If the encrypted message appears then it originated with the Server!*)
goal thy
- "!!evs. [| B ~: lost; evs : woolam |] \
-\ ==> Crypt (shrK B) {|Agent A, NB|} : parts (sees lost Spy evs) \
+ "!!evs. [| B ~: lost; evs : woolam |] \
+\ ==> Crypt (shrK B) {|Agent A, NB|} : parts (sees lost Spy evs) \
\ --> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs";
by parts_induct_tac;
by (Fake_parts_insert_tac 1);
@@ -143,7 +142,7 @@
(*Partial guarantee for B: if it gets a message of correct form then the Server
sent the same message.*)
goal thy
- "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, NB|}) : set evs; \
+ "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, NB|}) : set evs; \
\ B ~: lost; evs : woolam |] \
\ ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs";
by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
@@ -156,7 +155,7 @@
the Server via the Spy.*)
goal thy
"!!evs. [| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set evs; \
-\ A ~: lost; B ~: lost; evs : woolam |] \
+\ A ~: lost; B ~: lost; evs : woolam |] \
\ ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
by (blast_tac (!claset addIs [Server_trusts_WL4]
addSDs [B_got_WL5 RS Server_sent_WL5]) 1);
@@ -176,9 +175,9 @@
(**CANNOT be proved because A doesn't know where challenges come from...
goal thy
- "!!evs. [| A ~: lost; B ~= Spy; evs : woolam |] \
+ "!!evs. [| A ~: lost; B ~= Spy; evs : woolam |] \
\ ==> Crypt (shrK A) (Nonce NB) : parts (sees lost Spy evs) & \
-\ Says B A (Nonce NB) : set evs \
+\ Says B A (Nonce NB) : set evs \
\ --> Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
by parts_induct_tac;
by (Fake_parts_insert_tac 1);
--- a/src/HOL/Auth/Yahalom.ML Thu Jun 26 13:20:50 1997 +0200
+++ b/src/HOL/Auth/Yahalom.ML Fri Jun 27 10:47:13 1997 +0200
@@ -23,7 +23,7 @@
(*A "possibility property": there are traces that reach the end*)
goal thy
"!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
-\ ==> EX X NB K. EX evs: yahalom lost. \
+\ ==> EX X NB K. EX evs: yahalom lost. \
\ Says A B {|X, Crypt K (Nonce NB)|} : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS
@@ -39,7 +39,7 @@
by (rtac subsetI 1);
by (etac yahalom.induct 1);
by (REPEAT_FIRST
- (blast_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
+ (blast_tac (!claset addIs (impOfSubs(sees_mono RS analz_mono RS synth_mono)
:: yahalom.intrs))));
qed "yahalom_mono";
@@ -65,8 +65,7 @@
YM4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
(*Relates to both YM4 and Oops*)
-goal thy "!!evs. Says S A {|Crypt (shrK A) {|B, K, NA, NB|}, X|} \
-\ : set evs ==> \
+goal thy "!!evs. Says S A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} : set evs ==> \
\ K : parts (sees lost Spy evs)";
by (blast_tac (!claset addSEs partsEs
addSDs [Says_imp_sees_Spy' RS parts.Inj]) 1);
@@ -140,7 +139,7 @@
Oops as well as main secrecy property.*)
goal thy
"!!evs. [| Says Server A {|Crypt (shrK A) {|Agent B, Key K, NA, NB|}, X|} \
-\ : set evs; \
+\ : set evs; \
\ evs : yahalom lost |] \
\ ==> K ~: range shrK";
by (etac rev_mp 1);
@@ -169,8 +168,8 @@
(** Session keys are not used to encrypt other session keys **)
goal thy
- "!!evs. evs : yahalom lost ==> \
-\ ALL K KK. KK <= Compl (range shrK) --> \
+ "!!evs. evs : yahalom lost ==> \
+\ ALL K KK. KK <= Compl (range shrK) --> \
\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
\ (K : KK | Key K : analz (sees lost Spy evs))";
by (etac yahalom.induct 1);
@@ -186,7 +185,7 @@
goal thy
"!!evs. [| evs : yahalom lost; KAB ~: range shrK |] ==> \
-\ Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
+\ Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
\ (K = KAB | Key K : analz (sees lost Spy evs))";
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
qed "analz_insert_freshK";
@@ -196,7 +195,7 @@
goal thy
"!!evs. evs : yahalom lost ==> \
-\ EX A' B' na' nb' X'. ALL A B na nb X. \
+\ EX A' B' na' nb' X'. ALL A B na nb X. \
\ Says Server A \
\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \
\ : set evs --> A=A' & B=B' & na=na' & nb=nb' & X=X'";
@@ -216,10 +215,10 @@
goal thy
"!!evs. [| Says Server A \
\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \
-\ : set evs; \
+\ : set evs; \
\ Says Server A' \
\ {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|} \
-\ : set evs; \
+\ : set evs; \
\ evs : yahalom lost |] \
\ ==> A=A' & B=B' & na=na' & nb=nb'";
by (prove_unique_tac lemma 1);
@@ -233,8 +232,8 @@
\ ==> Says Server A \
\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, \
\ Crypt (shrK B) {|Agent A, Key K|}|} \
-\ : set evs --> \
-\ Says A Spy {|na, nb, Key K|} ~: set evs --> \
+\ : set evs --> \
+\ Says A Spy {|na, nb, Key K|} ~: set evs --> \
\ Key K ~: analz (sees lost Spy evs)";
by (etac yahalom.induct 1);
by analz_sees_tac;
@@ -259,8 +258,8 @@
"!!evs. [| Says Server A \
\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, \
\ Crypt (shrK B) {|Agent A, Key K|}|} \
-\ : set evs; \
-\ Says A Spy {|na, nb, Key K|} ~: set evs; \
+\ : set evs; \
+\ Says A Spy {|na, nb, Key K|} ~: set evs; \
\ A ~: lost; B ~: lost; evs : yahalom lost |] \
\ ==> Key K ~: analz (sees lost Spy evs)";
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
@@ -274,8 +273,8 @@
\ Says Server A \
\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, \
\ Crypt (shrK B) {|Agent A, Key K|}|} \
-\ : set evs; \
-\ Says A Spy {|na, nb, Key K|} ~: set evs; \
+\ : set evs; \
+\ Says A Spy {|na, nb, Key K|} ~: set evs; \
\ A ~: lost; B ~: lost; evs : yahalom lost |] \
\ ==> Key K ~: analz (sees lost C evs)";
by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
@@ -394,7 +393,7 @@
goalw thy [KeyWithNonce_def]
"!!evs. [| Says Server A \
\ {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB'|}, X|} \
-\ : set evs; \
+\ : set evs; \
\ NB ~= NB'; evs : yahalom lost |] \
\ ==> ~ KeyWithNonce K NB evs";
by (blast_tac (!claset addDs [unique_session_keys]) 1);
@@ -453,7 +452,7 @@
goal thy
"!!evs. [| Says Server A \
\ {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|} \
-\ : set evs; \
+\ : set evs; \
\ NB ~= NB'; KAB ~: range shrK; evs : yahalom lost |] \
\ ==> (Nonce NB : analz (insert (Key KAB) (sees lost Spy evs))) = \
\ (Nonce NB : analz (sees lost Spy evs))";
@@ -495,9 +494,9 @@
not_lost_tac to remove the assumption B' ~: lost.*)
goal thy
"!!evs.[| Says C D {|X, Crypt (shrK B) {|Agent A, Nonce NA, NB|}|} \
-\ : set evs; B ~: lost; \
+\ : set evs; B ~: lost; \
\ Says C' D' {|X', Crypt (shrK B') {|Agent A', Nonce NA', NB|}|} \
-\ : set evs; \
+\ : set evs; \
\ NB ~: analz (sees lost Spy evs); evs : yahalom lost |] \
\ ==> NA' = NA & A' = A & B' = B";
by (not_lost_tac "B'" 1);
@@ -527,8 +526,8 @@
(*The Server sends YM3 only in response to YM2.*)
goal thy
- "!!evs. [| Says Server A \
-\ {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} : set evs; \
+ "!!evs. [| Says Server A \
+\ {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} : set evs; \
\ evs : yahalom lost |] \
\ ==> EX B'. Says B' Server \
\ {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |} \
@@ -546,8 +545,8 @@
"!!evs. [| A ~: lost; B ~: lost; Spy: lost; evs : yahalom lost |] \
\ ==> Says B Server \
\ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
-\ : set evs --> \
-\ (ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs) --> \
+\ : set evs --> \
+\ (ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs) --> \
\ Nonce NB ~: analz (sees lost Spy evs)";
by (etac yahalom.induct 1);
by analz_sees_tac;
@@ -606,10 +605,10 @@
goal thy
"!!evs. [| Says B Server \
\ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
-\ : set evs; \
+\ : set evs; \
\ Says A' B {|Crypt (shrK B) {|Agent A, Key K|}, \
-\ Crypt K (Nonce NB)|} : set evs; \
-\ ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs; \
+\ Crypt K (Nonce NB)|} : set evs; \
+\ ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs; \
\ A ~: lost; B ~: lost; Spy: lost; evs : yahalom lost |] \
\ ==> Says Server A \
\ {|Crypt (shrK A) {|Agent B, Key K, \
@@ -636,8 +635,7 @@
\ ==> Crypt (shrK B) {|Agent A, Nonce NA, nb|} \
\ : parts (sees lost Spy evs) --> \
\ B ~: lost --> \
-\ Says B Server {|Agent B, \
-\ Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \
+\ Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \
\ : set evs";
by parts_induct_tac;
by (Fake_parts_insert_tac 1);
@@ -645,12 +643,11 @@
(*If the server sends YM3 then B sent YM2*)
goal thy
- "!!evs. evs : yahalom lost \
+ "!!evs. evs : yahalom lost \
\ ==> Says Server A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
-\ : set evs --> \
-\ B ~: lost --> \
-\ Says B Server {|Agent B, \
-\ Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \
+\ : set evs --> \
+\ B ~: lost --> \
+\ Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \
\ : set evs";
by (etac yahalom.induct 1);
by (ALLGOALS Asm_simp_tac);
@@ -664,7 +661,7 @@
(*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
goal thy
"!!evs. [| Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
-\ : set evs; \
+\ : set evs; \
\ A ~: lost; B ~: lost; evs : yahalom lost |] \
\ ==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \
\ : set evs";
@@ -720,11 +717,10 @@
goal thy
"!!evs. [| Says B Server \
\ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
-\ : set evs; \
-\ Says A' B {|Crypt (shrK B) {|Agent A, Key K|}, \
-\ Crypt K (Nonce NB)|} : set evs; \
-\ (ALL NA k. Says A Spy {|Nonce NA, Nonce NB, k|} \
-\ ~: set evs); \
+\ : set evs; \
+\ Says A' B {|Crypt (shrK B) {|Agent A, Key K|}, \
+\ Crypt K (Nonce NB)|} : set evs; \
+\ (ALL NA k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs); \
\ A ~: lost; B ~: lost; Spy: lost; evs : yahalom lost |] \
\ ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
by (dtac B_trusts_YM4 1);
--- a/src/HOL/Auth/Yahalom2.ML Thu Jun 26 13:20:50 1997 +0200
+++ b/src/HOL/Auth/Yahalom2.ML Fri Jun 27 10:47:13 1997 +0200
@@ -23,7 +23,7 @@
(*A "possibility property": there are traces that reach the end*)
goal thy
- "!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
+ "!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
\ ==> EX X NB K. EX evs: yahalom lost. \
\ Says A B {|X, Crypt K (Nonce NB)|} : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
@@ -66,11 +66,10 @@
YM4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
(*Relates to both YM4 and Oops*)
-goal thy "!!evs. Says S A {|NB, Crypt (shrK A) {|B, K, NA|}, X|} \
-\ : set evs ==> \
+goal thy "!!evs. Says S A {|NB, Crypt (shrK A) {|B,K,NA|}, X|} : set evs ==> \
\ K : parts (sees lost Spy evs)";
by (blast_tac (!claset addSEs partsEs
- addSDs [Says_imp_sees_Spy' RS parts.Inj]) 1);
+ addSDs [Says_imp_sees_Spy' RS parts.Inj]) 1);
qed "YM4_Key_parts_sees_Spy";
(*For proving the easier theorems about X ~: parts (sees lost Spy evs).
@@ -140,7 +139,7 @@
Oops as well as main secrecy property.*)
goal thy
"!!evs. [| Says Server A {|NB', Crypt (shrK A) {|Agent B, Key K, NA|}, X|} \
-\ : set evs; \
+\ : set evs; \
\ evs : yahalom lost |] \
\ ==> K ~: range shrK & A ~= B";
by (etac rev_mp 1);
@@ -170,9 +169,9 @@
(** Session keys are not used to encrypt other session keys **)
goal thy
- "!!evs. evs : yahalom lost ==> \
-\ ALL K KK. KK <= Compl (range shrK) --> \
-\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
+ "!!evs. evs : yahalom lost ==> \
+\ ALL K KK. KK <= Compl (range shrK) --> \
+\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
\ (K : KK | Key K : analz (sees lost Spy evs))";
by (etac yahalom.induct 1);
by analz_sees_tac;
@@ -187,7 +186,7 @@
goal thy
"!!evs. [| evs : yahalom lost; KAB ~: range shrK |] ==> \
-\ Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
+\ Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
\ (K = KAB | Key K : analz (sees lost Spy evs))";
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
qed "analz_insert_freshK";
@@ -216,10 +215,10 @@
goal thy
"!!evs. [| Says Server A \
\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|} \
-\ : set evs; \
+\ : set evs; \
\ Says Server A' \
\ {|nb', Crypt (shrK A') {|Agent B', Key K, na'|}, X'|} \
-\ : set evs; \
+\ : set evs; \
\ evs : yahalom lost |] \
\ ==> A=A' & B=B' & na=na' & nb=nb'";
by (prove_unique_tac lemma 1);
@@ -234,8 +233,8 @@
\ ==> Says Server A \
\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, \
\ Crypt (shrK B) {|nb, Key K, Agent A|}|} \
-\ : set evs --> \
-\ Says A Spy {|na, nb, Key K|} ~: set evs --> \
+\ : set evs --> \
+\ Says A Spy {|na, nb, Key K|} ~: set evs --> \
\ Key K ~: analz (sees lost Spy evs)";
by (etac yahalom.induct 1);
by analz_sees_tac;
@@ -260,8 +259,8 @@
"!!evs. [| Says Server A \
\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, \
\ Crypt (shrK B) {|nb, Key K, Agent A|}|} \
-\ : set evs; \
-\ Says A Spy {|na, nb, Key K|} ~: set evs; \
+\ : set evs; \
+\ Says A Spy {|na, nb, Key K|} ~: set evs; \
\ A ~: lost; B ~: lost; evs : yahalom lost |] \
\ ==> Key K ~: analz (sees lost Spy evs)";
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
@@ -275,8 +274,8 @@
\ Says Server A \
\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, \
\ Crypt (shrK B) {|nb, Key K, Agent A|}|} \
-\ : set evs; \
-\ Says A Spy {|na, nb, Key K|} ~: set evs; \
+\ : set evs; \
+\ Says A Spy {|na, nb, Key K|} ~: set evs; \
\ A ~: lost; B ~: lost; evs : yahalom lost |] \
\ ==> Key K ~: analz (sees lost C evs)";
by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
@@ -333,7 +332,7 @@
because we do not have to show that NB is secret. *)
goal thy
"!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|}, X|} \
-\ : set evs; \
+\ : set evs; \
\ A ~: lost; B ~: lost; evs : yahalom lost |] \
\ ==> EX NA. Says Server A \
\ {|Nonce NB, \
@@ -364,9 +363,9 @@
(*If the server sends YM3 then B sent YM2, perhaps with a different NB*)
goal thy
- "!!evs. evs : yahalom lost \
+ "!!evs. evs : yahalom lost \
\ ==> Says Server A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \
-\ : set evs --> \
+\ : set evs --> \
\ B ~: lost --> \
\ (EX nb'. Says B Server {|Agent B, nb', \
\ Crypt (shrK B) {|Agent A, Nonce NA|}|} \
@@ -384,7 +383,7 @@
(*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
goal thy
"!!evs. [| Says S A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \
-\ : set evs; \
+\ : set evs; \
\ A ~: lost; B ~: lost; evs : yahalom lost |] \
\ ==> EX nb'. Says B Server \
\ {|Agent B, nb', Crypt (shrK B) {|Agent A, Nonce NA|}|} \
@@ -440,7 +439,7 @@
Other premises guarantee secrecy of K.*)
goal thy
"!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|}, \
-\ Crypt K (Nonce NB)|} : set evs; \
+\ Crypt K (Nonce NB)|} : set evs; \
\ (ALL NA. Says A Spy {|Nonce NA, Nonce NB, Key K|} ~: set evs); \
\ A ~: lost; B ~: lost; evs : yahalom lost |] \
\ ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
--- a/src/HOL/Auth/Yahalom2.thy Thu Jun 26 13:20:50 1997 +0200
+++ b/src/HOL/Auth/Yahalom2.thy Fri Jun 27 10:47:13 1997 +0200
@@ -57,8 +57,7 @@
uses the new session key to send Bob his Nonce.*)
YM4 "[| evs: yahalom lost; A ~= Server; A ~= B;
Says S A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
- X|}
- : set evs;
+ X|} : set evs;
Says A B {|Agent A, Nonce NA|} : set evs |]
==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom lost"