src/HOL/Auth/OtwayRees.ML
changeset 5278 a903b66822e2
parent 5223 4cb05273f764
child 5359 bd539b72d484
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Thu Aug 06 15:47:26 1998 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Thu Aug 06 15:48:13 1998 +0200
     1.3 @@ -18,8 +18,7 @@
     1.4  
     1.5  
     1.6  (*A "possibility property": there are traces that reach the end*)
     1.7 -Goal 
     1.8 - "[| A ~= B; A ~= Server; B ~= Server |]   \
     1.9 +Goal "[| A ~= B; A ~= Server; B ~= Server |]   \
    1.10  \     ==> EX K. EX NA. EX evs: otway.          \
    1.11  \            Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
    1.12  \              : set evs";
    1.13 @@ -77,15 +76,13 @@
    1.14      sends messages containing X! **)
    1.15  
    1.16  (*Spy never sees a good agent's shared key!*)
    1.17 -Goal 
    1.18 - "evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
    1.19 +Goal "evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
    1.20  by (parts_induct_tac 1);
    1.21  by (ALLGOALS Blast_tac);
    1.22  qed "Spy_see_shrK";
    1.23  Addsimps [Spy_see_shrK];
    1.24  
    1.25 -Goal 
    1.26 - "evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
    1.27 +Goal "evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
    1.28  by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
    1.29  qed "Spy_analz_shrK";
    1.30  Addsimps [Spy_analz_shrK];
    1.31 @@ -116,8 +113,7 @@
    1.32  
    1.33  (*Describes the form of K and NA when the Server sends this message.  Also
    1.34    for Oops case.*)
    1.35 -Goal 
    1.36 - "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
    1.37 +Goal "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
    1.38  \    evs : otway |]                                           \
    1.39  \     ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
    1.40  by (etac rev_mp 1);
    1.41 @@ -148,8 +144,7 @@
    1.42  (** Session keys are not used to encrypt other session keys **)
    1.43  
    1.44  (*The equality makes the induction hypothesis easier to apply*)
    1.45 -Goal  
    1.46 - "evs : otway ==>                                    \
    1.47 +Goal "evs : otway ==>                                    \
    1.48  \  ALL K KK. KK <= Compl (range shrK) -->                   \
    1.49  \     (Key K : analz (Key``KK Un (spies evs))) =  \
    1.50  \     (K : KK | Key K : analz (spies evs))";
    1.51 @@ -163,8 +158,7 @@
    1.52  qed_spec_mp "analz_image_freshK";
    1.53  
    1.54  
    1.55 -Goal
    1.56 - "[| evs : otway;  KAB ~: range shrK |] ==>          \
    1.57 +Goal "[| evs : otway;  KAB ~: range shrK |] ==>          \
    1.58  \ Key K : analz (insert (Key KAB) (spies evs)) =  \
    1.59  \ (K = KAB | Key K : analz (spies evs))";
    1.60  by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
    1.61 @@ -173,8 +167,7 @@
    1.62  
    1.63  (*** The Key K uniquely identifies the Server's  message. **)
    1.64  
    1.65 -Goal 
    1.66 - "evs : otway ==>                                                  \
    1.67 +Goal "evs : otway ==>                                                  \
    1.68  \   EX B' NA' NB' X'. ALL B NA NB X.                                      \
    1.69  \     Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs -->     \
    1.70  \     B=B' & NA=NA' & NB=NB' & X=X'";
    1.71 @@ -190,8 +183,7 @@
    1.72  by (blast_tac (claset() addSEs spies_partsEs) 1);
    1.73  val lemma = result();
    1.74  
    1.75 -Goal 
    1.76 - "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|}   : set evs; \ 
    1.77 +Goal "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|}   : set evs; \ 
    1.78  \    Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} : set evs; \
    1.79  \    evs : otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
    1.80  by (prove_unique_tac lemma 1);
    1.81 @@ -202,8 +194,7 @@
    1.82  (**** Authenticity properties relating to NA ****)
    1.83  
    1.84  (*Only OR1 can have caused such a part of a message to appear.*)
    1.85 -Goal 
    1.86 - "[| A ~: bad;  evs : otway |]                             \
    1.87 +Goal "[| A ~: bad;  evs : otway |]                             \
    1.88  \ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \
    1.89  \     Says A B {|NA, Agent A, Agent B,                      \
    1.90  \                Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \
    1.91 @@ -215,8 +206,7 @@
    1.92  
    1.93  (** The Nonce NA uniquely identifies A's message. **)
    1.94  
    1.95 -Goal 
    1.96 - "[| evs : otway; A ~: bad |]               \
    1.97 +Goal "[| evs : otway; A ~: bad |]               \
    1.98  \ ==> EX B'. ALL B.                                 \
    1.99  \        Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) \
   1.100  \        --> B = B'";
   1.101 @@ -228,8 +218,7 @@
   1.102  by (Blast_tac 1);
   1.103  val lemma = result();
   1.104  
   1.105 -Goal 
   1.106 - "[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts (spies evs); \
   1.107 +Goal "[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts (spies evs); \
   1.108  \          Crypt (shrK A) {|NA, Agent A, Agent C|}: parts (spies evs); \
   1.109  \          evs : otway;  A ~: bad |]                                   \
   1.110  \        ==> B = C";
   1.111 @@ -240,8 +229,7 @@
   1.112  (*It is impossible to re-use a nonce in both OR1 and OR2.  This holds because
   1.113    OR2 encrypts Nonce NB.  It prevents the attack that can occur in the
   1.114    over-simplified version of this protocol: see OtwayRees_Bad.*)
   1.115 -Goal 
   1.116 - "[| A ~: bad;  evs : otway |]                      \
   1.117 +Goal "[| A ~: bad;  evs : otway |]                      \
   1.118  \        ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \
   1.119  \            Crypt (shrK A) {|NA', NA, Agent A', Agent A|}  \
   1.120  \             ~: parts (spies evs)";
   1.121 @@ -253,8 +241,7 @@
   1.122  
   1.123  (*Crucial property: If the encrypted message appears, and A has used NA
   1.124    to start a run, then it originated with the Server!*)
   1.125 -Goal 
   1.126 - "[| A ~: bad;  evs : otway |]                                  \
   1.127 +Goal "[| A ~: bad;  evs : otway |]                                  \
   1.128  \    ==> Crypt (shrK A) {|NA, Key K|} : parts (spies evs)              \
   1.129  \        --> Says A B {|NA, Agent A, Agent B,                          \
   1.130  \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}      \
   1.131 @@ -285,8 +272,7 @@
   1.132    then the key really did come from the Server!  CANNOT prove this of the
   1.133    bad form of this protocol, even though we can prove
   1.134    Spy_not_see_encrypted_key*)
   1.135 -Goal 
   1.136 - "[| Says A  B {|NA, Agent A, Agent B,                       \
   1.137 +Goal "[| Says A  B {|NA, Agent A, Agent B,                       \
   1.138  \                Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
   1.139  \    Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
   1.140  \    A ~: bad;  evs : otway |]                              \
   1.141 @@ -303,8 +289,7 @@
   1.142      Does not in itself guarantee security: an attack could violate 
   1.143      the premises, e.g. by having A=Spy **)
   1.144  
   1.145 -Goal 
   1.146 - "[| A ~: bad;  B ~: bad;  evs : otway |]                      \
   1.147 +Goal "[| A ~: bad;  B ~: bad;  evs : otway |]                      \
   1.148  \ ==> Says Server B                                            \
   1.149  \       {|NA, Crypt (shrK A) {|NA, Key K|},                    \
   1.150  \         Crypt (shrK B) {|NB, Key K|}|} : set evs -->         \
   1.151 @@ -353,8 +338,7 @@
   1.152  
   1.153  (*Only OR2 can have caused such a part of a message to appear.  We do not
   1.154    know anything about X: it does NOT have to have the right form.*)
   1.155 -Goal 
   1.156 - "[| B ~: bad;  evs : otway |]                         \
   1.157 +Goal "[| B ~: bad;  evs : otway |]                         \
   1.158  \     ==> Crypt (shrK B) {|NA, NB, Agent A, Agent B|}       \
   1.159  \          : parts (spies evs) -->                       \
   1.160  \         (EX X. Says B Server                              \
   1.161 @@ -380,8 +364,7 @@
   1.162  by (Blast_tac 1);
   1.163  val lemma = result();
   1.164  
   1.165 -Goal 
   1.166 - "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(spies evs); \
   1.167 +Goal "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(spies evs); \
   1.168  \          Crypt (shrK B) {|NC, NB, Agent C, Agent B|} : parts(spies evs); \
   1.169  \          evs : otway;  B ~: bad |]             \
   1.170  \        ==> NC = NA & C = A";