src/HOL/Auth/OtwayRees_AN.ML
changeset 3466 30791e5a69c4
parent 3465 e85c24717cad
child 3516 470626799511
     1.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Thu Jun 26 13:20:50 1997 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Fri Jun 27 10:47:13 1997 +0200
     1.3 @@ -139,7 +139,7 @@
     1.4   "!!evs. [| Says Server B                                           \
     1.5  \              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
     1.6  \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
     1.7 -\             : set evs;                                    \
     1.8 +\             : set evs;                                            \
     1.9  \           evs : otway lost |]                                     \
    1.10  \        ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
    1.11  by (etac rev_mp 1);
    1.12 @@ -171,9 +171,9 @@
    1.13  
    1.14  (*The equality makes the induction hypothesis easier to apply*)
    1.15  goal thy  
    1.16 - "!!evs. evs : otway lost ==>                                         \
    1.17 -\  ALL K KK. KK <= Compl (range shrK) -->                      \
    1.18 -\            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
    1.19 + "!!evs. evs : otway lost ==>                                    \
    1.20 +\  ALL K KK. KK <= Compl (range shrK) -->                        \
    1.21 +\            (Key K : analz (Key``KK Un (sees lost Spy evs))) =  \
    1.22  \            (K : KK | Key K : analz (sees lost Spy evs))";
    1.23  by (etac otway.induct 1);
    1.24  by analz_sees_tac;
    1.25 @@ -188,8 +188,8 @@
    1.26  
    1.27  
    1.28  goal thy
    1.29 - "!!evs. [| evs : otway lost;  KAB ~: range shrK |] ==>             \
    1.30 -\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
    1.31 + "!!evs. [| evs : otway lost;  KAB ~: range shrK |] ==>          \
    1.32 +\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) =  \
    1.33  \        (K = KAB | Key K : analz (sees lost Spy evs))";
    1.34  by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
    1.35  qed "analz_insert_freshK";
    1.36 @@ -200,8 +200,8 @@
    1.37  goal thy 
    1.38   "!!evs. evs : otway lost ==>                              \
    1.39  \      EX A' B' NA' NB'. ALL A B NA NB.                    \
    1.40 -\       Says Server B \
    1.41 -\         {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},                     \
    1.42 +\       Says Server B                                      \
    1.43 +\         {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},             \
    1.44  \           Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set evs  \
    1.45  \       --> A=A' & B=B' & NA=NA' & NB=NB'";
    1.46  by (etac otway.induct 1);
    1.47 @@ -222,11 +222,11 @@
    1.48  "!!evs. [| Says Server 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 evs;                                     \
    1.52 +\           : set evs;                                             \
    1.53  \          Says Server B'                                          \
    1.54  \            {|Crypt (shrK A') {|NA', Agent A', Agent B', K|},     \
    1.55  \              Crypt (shrK B') {|NB', Agent A', Agent B', K|}|}    \
    1.56 -\           : set evs;                                     \
    1.57 +\           : set evs;                                             \
    1.58  \          evs : otway lost |]                                     \
    1.59  \       ==> A=A' & B=B' & NA=NA' & NB=NB'";
    1.60  by (prove_unique_tac lemma 1);
    1.61 @@ -257,7 +257,7 @@
    1.62    Freshness may be inferred from nonce NA.*)
    1.63  goal thy 
    1.64   "!!evs. [| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|})  \
    1.65 -\            : set evs;                                         \
    1.66 +\            : set evs;                                                 \
    1.67  \           A ~: lost;  evs : otway lost |]                             \
    1.68  \        ==> EX NB. Says Server B                                       \
    1.69  \                    {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},  \
    1.70 @@ -277,8 +277,8 @@
    1.71  \        ==> Says Server B                                                 \
    1.72  \             {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},            \
    1.73  \               Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}           \
    1.74 -\            : set evs -->                                         \
    1.75 -\            Says B Spy {|NA, NB, Key K|} ~: set evs -->           \
    1.76 +\            : set evs -->                                                 \
    1.77 +\            Says B Spy {|NA, NB, Key K|} ~: set evs -->                   \
    1.78  \            Key K ~: analz (sees lost Spy evs)";
    1.79  by (etac otway.induct 1);
    1.80  by analz_sees_tac;
    1.81 @@ -302,8 +302,8 @@
    1.82   "!!evs. [| Says Server B                                           \
    1.83  \              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
    1.84  \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
    1.85 -\             : set evs;                                    \
    1.86 -\           Says B Spy {|NA, NB, Key K|} ~: set evs;        \
    1.87 +\             : set evs;                                            \
    1.88 +\           Says B Spy {|NA, NB, Key K|} ~: set evs;                \
    1.89  \           A ~: lost;  B ~: lost;  evs : otway lost |]             \
    1.90  \        ==> Key K ~: analz (sees lost Spy evs)";
    1.91  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
    1.92 @@ -316,8 +316,8 @@
    1.93  \           Says Server B                                           \
    1.94  \              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
    1.95  \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
    1.96 -\             : set evs;                                    \
    1.97 -\           Says B Spy {|NA, NB, Key K|} ~: set evs;        \
    1.98 +\             : set evs;                                            \
    1.99 +\           Says B Spy {|NA, NB, Key K|} ~: set evs;                \
   1.100  \           A ~: lost;  B ~: lost;  evs : otway lost |]             \
   1.101  \        ==> Key K ~: analz (sees lost C evs)";
   1.102  by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   1.103 @@ -351,7 +351,7 @@
   1.104  goal thy 
   1.105   "!!evs. [| B ~: lost;  evs : otway lost;                                   \
   1.106  \           Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
   1.107 -\            : set evs |]                                           \
   1.108 +\            : set evs |]                                                   \
   1.109  \        ==> EX NA. Says Server B                                           \
   1.110  \                     {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
   1.111  \                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \