src/HOL/Auth/Yahalom.ML
changeset 2001 974167c1d2c4
parent 1995 c80e58e78d9c
child 2013 4b7a432fb3ed
     1.1 --- a/src/HOL/Auth/Yahalom.ML	Fri Sep 13 18:48:25 1996 +0200
     1.2 +++ b/src/HOL/Auth/Yahalom.ML	Fri Sep 13 18:49:43 1996 +0200
     1.3 @@ -78,8 +78,8 @@
     1.4  
     1.5  (*Enemy never sees another agent's shared key! (unless it is leaked at start)*)
     1.6  goal thy 
     1.7 - "!!evs. [| evs : yahalom;  A ~: bad |] ==> \
     1.8 -\        Key (shrK A) ~: parts (sees Enemy evs)";
     1.9 + "!!evs. [| evs : yahalom;  A ~: bad |]    \
    1.10 +\        ==> Key (shrK A) ~: parts (sees Enemy evs)";
    1.11  be yahalom.induct 1;
    1.12  bd (YM4_analz_sees_Enemy RS synth.Inj) 6;
    1.13  by (ALLGOALS Asm_simp_tac);
    1.14 @@ -135,8 +135,8 @@
    1.15  
    1.16  (*Variant needed for the main theorem below*)
    1.17  goal thy 
    1.18 - "!!evs. [| evs : yahalom;  length evs <= length evs' |] ==> \
    1.19 -\        Key (newK evs') ~: parts (sees C evs)";
    1.20 + "!!evs. [| evs : yahalom;  length evs <= length evs' |]    \
    1.21 +\        ==> Key (newK evs') ~: parts (sees C evs)";
    1.22  by (fast_tac (!claset addDs [lemma]) 1);
    1.23  qed "new_keys_not_seen";
    1.24  Addsimps [new_keys_not_seen];
    1.25 @@ -180,8 +180,8 @@
    1.26  val lemma = result();
    1.27  
    1.28  goal thy 
    1.29 - "!!evs. [| evs : yahalom;  length evs <= length evs' |] ==> \
    1.30 -\        newK evs' ~: keysFor (parts (sees C evs))";
    1.31 + "!!evs. [| evs : yahalom;  length evs <= length evs' |]    \
    1.32 +\        ==> newK evs' ~: keysFor (parts (sees C evs))";
    1.33  by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
    1.34  qed "new_keys_not_used";
    1.35  
    1.36 @@ -344,3 +344,62 @@
    1.37  (*Fake*) (** LEVEL 10 **)
    1.38  by (enemy_analz_tac 1);
    1.39  qed "Enemy_not_see_encrypted_key";
    1.40 +
    1.41 +
    1.42 +goal thy 
    1.43 + "!!evs. [| Crypt {|Agent A, Key K|} (shrK B) : analz (sees Enemy evs); \
    1.44 +\           B ~: bad;  evs : yahalom |]                                 \
    1.45 +\        ==> EX NA NB. Says Server A                                    \
    1.46 +\                     {|Crypt {|Agent B, Key K,                         \
    1.47 +\                               Nonce NA, Nonce NB|} (shrK A),          \
    1.48 +\                       Crypt {|Agent A, Key K|} (shrK B)|}             \
    1.49 +\                   : set_of_list evs";
    1.50 +be rev_mp 1;
    1.51 +be yahalom.induct 1;
    1.52 +by (forward_tac [YM4_analz_sees_Enemy] 6);
    1.53 +by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
    1.54 +(*YM4*)
    1.55 +by (enemy_analz_tac 4);
    1.56 +(*YM3*)
    1.57 +by (Fast_tac 3);
    1.58 +(*Fake*)
    1.59 +by (enemy_analz_tac 2);
    1.60 +(*Base case*)
    1.61 +by (fast_tac (!claset addss (!simpset)) 1);
    1.62 +qed "Enemy_analz_Server_msg";
    1.63 +
    1.64 +
    1.65 +(*What can B deduce from receipt of YM4?  
    1.66 +  NOT THAT THE NONCES AGREE (in this version).  But what does the Nonce
    1.67 +	give us??*)
    1.68 +goal thy 
    1.69 + "!!evs. [| Says A' B {|Crypt {|Agent A, Key K|} (shrK B),              \
    1.70 +\                       Crypt (Nonce NB) K|} : set_of_list evs;         \
    1.71 +\           B ~: bad;  evs : yahalom |]                                 \
    1.72 +\        ==> EX NA NB. Says Server A                                    \
    1.73 +\                     {|Crypt {|Agent B, Key K,                         \
    1.74 +\                               Nonce NA, Nonce NB|} (shrK A),          \
    1.75 +\                       Crypt {|Agent A, Key K|} (shrK B)|}             \
    1.76 +\                   : set_of_list evs";
    1.77 +be rev_mp 1;
    1.78 +be yahalom.induct 1;
    1.79 +by (forward_tac [YM4_analz_sees_Enemy] 6);
    1.80 +by (ALLGOALS Asm_simp_tac);
    1.81 +(*YM4*)
    1.82 +by (fast_tac (!claset addSDs [Enemy_analz_Server_msg]) 3);
    1.83 +(*YM3*)
    1.84 +by (Fast_tac 2);
    1.85 +(*Fake*)
    1.86 +by (fast_tac (!claset addSDs [Enemy_analz_Server_msg]) 1);
    1.87 +qed "YM4_imp_Says_Server_A";
    1.88 +
    1.89 +
    1.90 +
    1.91 +goal thy 
    1.92 + "!!evs. [| Says A' B {|Crypt {|Agent A, Key K|} (shrK B),              \
    1.93 +\                       Crypt (Nonce NB) K|} : set_of_list evs;         \
    1.94 +\           A ~: bad;  B ~: bad;  evs : yahalom |]                      \
    1.95 +\        ==> Key K ~: analz (sees Enemy evs)";
    1.96 +by (fast_tac (!claset addSDs [YM4_imp_Says_Server_A,
    1.97 +			      Enemy_not_see_encrypted_key]) 1);
    1.98 +qed "B_gets_secure_key";