src/HOL/Auth/OtwayRees_AN.ML
changeset 2284 80ebd1a213fd
parent 2264 f298678bd54a
child 2331 d6a56ff0d94e
     1.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Fri Nov 29 17:58:18 1996 +0100
     1.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Fri Nov 29 18:03:21 1996 +0100
     1.3 @@ -22,7 +22,7 @@
     1.4  goal thy 
     1.5   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
     1.6  \        ==> EX K. EX NA. EX evs: otway lost.          \
     1.7 -\             Says B A (Crypt {|Nonce NA, Agent A, Agent B, Key K|} (shrK A)) \
     1.8 +\             Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \
     1.9  \             : set_of_list evs";
    1.10  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.11  by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
    1.12 @@ -59,7 +59,7 @@
    1.13  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    1.14  qed "OR4_analz_sees_Spy";
    1.15  
    1.16 -goal thy "!!evs. Says Server B {|X, Crypt {|NB, a, Agent B, K|} K'|} \
    1.17 +goal thy "!!evs. Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} \
    1.18  \                  : set_of_list evs ==> K : parts (sees lost Spy evs)";
    1.19  by (fast_tac (!claset addSEs partsEs
    1.20                        addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
    1.21 @@ -176,8 +176,8 @@
    1.22  (*Describes the form of K and NA when the Server sends this message.*)
    1.23  goal thy 
    1.24   "!!evs. [| Says Server B \
    1.25 -\           {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),                    \
    1.26 -\             Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs; \
    1.27 +\           {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},                    \
    1.28 +\             Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs; \
    1.29  \           evs : otway lost |]                                        \
    1.30  \        ==> (EX evt: otway lost. K = Key(newK evt)) &                  \
    1.31  \            (EX i. NA = Nonce i) &                  \
    1.32 @@ -246,8 +246,8 @@
    1.33   "!!evs. evs : otway lost ==>                      \
    1.34  \      EX A' B' NA' NB'. ALL A B NA NB.                    \
    1.35  \       Says Server B \
    1.36 -\         {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),                    \
    1.37 -\           Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs  \
    1.38 +\         {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},                    \
    1.39 +\           Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs  \
    1.40  \       --> A=A' & B=B' & NA=NA' & NB=NB'";
    1.41  by (etac otway.induct 1);
    1.42  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
    1.43 @@ -266,12 +266,12 @@
    1.44  
    1.45  goal thy 
    1.46  "!!evs. [| Says Server B                                           \
    1.47 -\            {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),         \
    1.48 -\              Crypt {|NB, Agent A, Agent B, K|} (shrK B)|}        \
    1.49 +\            {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},         \
    1.50 +\              Crypt (shrK B) {|NB, Agent A, Agent B, K|}|}        \
    1.51  \           : set_of_list evs;                                     \
    1.52  \          Says Server B'                                          \
    1.53 -\            {|Crypt {|NA', Agent A', Agent B', K|} (shrK A'),     \
    1.54 -\              Crypt {|NB', Agent A', Agent B', K|} (shrK B')|}    \
    1.55 +\            {|Crypt (shrK A') {|NA', Agent A', Agent B', K|},     \
    1.56 +\              Crypt (shrK B') {|NB', Agent A', Agent B', K|}|}    \
    1.57  \           : set_of_list evs;                                     \
    1.58  \          evs : otway lost |]                                     \
    1.59  \       ==> A=A' & B=B' & NA=NA' & NB=NB'";
    1.60 @@ -289,11 +289,11 @@
    1.61  (*If the encrypted message appears then it originated with the Server!*)
    1.62  goal thy 
    1.63   "!!evs. [| A ~: lost;  evs : otway lost |]                 \
    1.64 -\ ==> Crypt {|NA, Agent A, Agent B, Key K|} (shrK A)        \
    1.65 +\ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}        \
    1.66  \      : parts (sees lost Spy evs)                          \
    1.67  \     --> (EX NB. Says Server B                                     \
    1.68 -\                  {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A),     \
    1.69 -\                    Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|}    \
    1.70 +\                  {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
    1.71 +\                    Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
    1.72  \                  : set_of_list evs)";
    1.73  by (parts_induct_tac 1);
    1.74  by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
    1.75 @@ -308,12 +308,12 @@
    1.76    Spy_not_see_encrypted_key.  (We can implicitly infer freshness of
    1.77    the Server's message from its nonce NA.)*)
    1.78  goal thy 
    1.79 - "!!evs. [| Says B' A (Crypt {|NA, Agent A, Agent B, Key K|} (shrK A))  \
    1.80 + "!!evs. [| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|})  \
    1.81  \            : set_of_list evs;                                         \
    1.82  \           A ~: lost;  evs : otway lost |]                             \
    1.83  \        ==> EX NB. Says Server B                                       \
    1.84 -\                    {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A),  \
    1.85 -\                      Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|} \
    1.86 +\                    {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},  \
    1.87 +\                      Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
    1.88  \                   : set_of_list evs";
    1.89  by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
    1.90                        addEs  partsEs
    1.91 @@ -328,8 +328,8 @@
    1.92  goal thy 
    1.93   "!!evs. [| A ~: lost;  B ~: lost;  evs : otway lost |]                    \
    1.94  \        ==> Says Server B                                                 \
    1.95 -\             {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A),            \
    1.96 -\               Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|}           \
    1.97 +\             {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},            \
    1.98 +\               Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}           \
    1.99  \            : set_of_list evs -->                                         \
   1.100  \            Says B Spy {|NA, NB, Key K|} ~: set_of_list evs -->           \
   1.101  \            Key K ~: analz (sees lost Spy evs)";
   1.102 @@ -351,8 +351,8 @@
   1.103  
   1.104  goal thy 
   1.105   "!!evs. [| Says Server B                                                     \
   1.106 -\            {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),                    \
   1.107 -\              Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs;\
   1.108 +\            {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},                    \
   1.109 +\              Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs;\
   1.110  \           Says B Spy {|NA, NB, K|} ~: set_of_list evs;                      \
   1.111  \           A ~: lost;  B ~: lost;  evs : otway lost |]                       \
   1.112  \        ==> K ~: analz (sees lost Spy evs)";
   1.113 @@ -364,8 +364,8 @@
   1.114  goal thy 
   1.115   "!!evs. [| C ~: {A,B,Server};                                                \
   1.116  \           Says Server B                                                     \
   1.117 -\            {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),                    \
   1.118 -\              Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs;\
   1.119 +\            {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},                    \
   1.120 +\              Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs;\
   1.121  \           Says B Spy {|NA, NB, K|} ~: set_of_list evs;                 \
   1.122  \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   1.123  \        ==> K ~: analz (sees lost C evs)";
   1.124 @@ -381,11 +381,11 @@
   1.125  (*If the encrypted message appears then it originated with the Server!*)
   1.126  goal thy 
   1.127   "!!evs. [| B ~: lost;  evs : otway lost |]                                 \
   1.128 -\    ==> Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)                     \
   1.129 +\    ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}                     \
   1.130  \         : parts (sees lost Spy evs)                                       \
   1.131  \        --> (EX NA. Says Server B                                          \
   1.132 -\                     {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A),     \
   1.133 -\                       Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|}    \
   1.134 +\                     {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
   1.135 +\                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
   1.136  \                     : set_of_list evs)";
   1.137  by (parts_induct_tac 1);
   1.138  by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   1.139 @@ -398,11 +398,11 @@
   1.140    has sent the correct message.*)
   1.141  goal thy 
   1.142   "!!evs. [| B ~: lost;  evs : otway lost;                                   \
   1.143 -\           Says S B {|X, Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|}  \
   1.144 +\           Says S B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}  \
   1.145  \            : set_of_list evs |]                                           \
   1.146  \        ==> EX NA. Says Server B                                           \
   1.147 -\                     {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A),     \
   1.148 -\                       Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|}    \
   1.149 +\                     {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
   1.150 +\                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
   1.151  \                     : set_of_list evs";
   1.152  by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   1.153                        addEs  partsEs