Cosmetic changes: margins, indentation, ...
authorpaulson
Tue Jul 22 11:26:02 1997 +0200 (1997-07-22)
changeset 354382f33248d89d
parent 3542 db5e9aceea49
child 3544 6ae62d55a620
Cosmetic changes: margins, indentation, ...
src/HOL/Auth/OtwayRees.ML
src/HOL/Auth/OtwayRees_AN.ML
src/HOL/Auth/Yahalom.ML
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Tue Jul 22 11:23:03 1997 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Tue Jul 22 11:26:02 1997 +0200
     1.3 @@ -209,10 +209,8 @@
     1.4  val lemma = result();
     1.5  
     1.6  goal thy 
     1.7 - "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|}      \
     1.8 -\            : set evs;                                            \ 
     1.9 -\           Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|}    \
    1.10 -\            : set evs;                                            \
    1.11 + "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|}   : set evs; \ 
    1.12 +\           Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} : set evs; \
    1.13  \           evs : otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
    1.14  by (prove_unique_tac lemma 1);
    1.15  qed "unique_session_keys";
    1.16 @@ -277,8 +275,8 @@
    1.17  (*Crucial property: If the encrypted message appears, and A has used NA
    1.18    to start a run, then it originated with the Server!*)
    1.19  goal thy 
    1.20 - "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway |]                 \
    1.21 -\    ==> Crypt (shrK A) {|NA, Key K|} : parts (sees Spy evs)      \
    1.22 + "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway |]                      \
    1.23 +\    ==> Crypt (shrK A) {|NA, Key K|} : parts (sees Spy evs)           \
    1.24  \        --> Says A B {|NA, Agent A, Agent B,                          \
    1.25  \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}      \
    1.26  \             : set evs -->                                            \
    1.27 @@ -295,8 +293,8 @@
    1.28  (*OR4*)
    1.29  by (REPEAT (Safe_step_tac 2));
    1.30  by (REPEAT (blast_tac (!claset addSDs [parts_cut]) 3));
    1.31 -by (fast_tac (!claset addSIs [Crypt_imp_OR1]
    1.32 -                      addEs  sees_Spy_partsEs) 2);
    1.33 +by (blast_tac (!claset addSIs [Crypt_imp_OR1]
    1.34 +                       addEs  sees_Spy_partsEs) 2);
    1.35  (*OR3*)  (** LEVEL 5 **)
    1.36  by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1);
    1.37  by (step_tac (!claset delrules [disjCI, impCE]) 1);
     2.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Tue Jul 22 11:23:03 1997 +0200
     2.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Tue Jul 22 11:26:02 1997 +0200
     2.3 @@ -21,7 +21,7 @@
     2.4  (*A "possibility property": there are traces that reach the end*)
     2.5  goal thy 
     2.6   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]                               \
     2.7 -\        ==> EX K. EX NA. EX evs: otway.                                 \
     2.8 +\        ==> EX K. EX NA. EX evs: otway.                                      \
     2.9  \             Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \
    2.10  \             : set evs";
    2.11  by (REPEAT (resolve_tac [exI,bexI] 1));
    2.12 @@ -125,7 +125,7 @@
    2.13  \              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
    2.14  \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
    2.15  \             : set evs;                                            \
    2.16 -\           evs : otway |]                                     \
    2.17 +\           evs : otway |]                                          \
    2.18  \        ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
    2.19  by (etac rev_mp 1);
    2.20  by (etac otway.induct 1);
    2.21 @@ -183,9 +183,9 @@
    2.22  (*** The Key K uniquely identifies the Server's  message. **)
    2.23  
    2.24  goal thy 
    2.25 - "!!evs. evs : otway ==>                                   \
    2.26 -\      EX A' B' NA' NB'. ALL A B NA NB.                    \
    2.27 -\       Says Server B                                      \
    2.28 + "!!evs. evs : otway ==>                                            \
    2.29 +\      EX A' B' NA' NB'. ALL A B NA NB.                             \
    2.30 +\       Says Server B                                               \
    2.31  \         {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},             \
    2.32  \           Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set evs  \
    2.33  \       --> A=A' & B=B' & NA=NA' & NB=NB'";
    2.34 @@ -258,12 +258,12 @@
    2.35      the premises, e.g. by having A=Spy **)
    2.36  
    2.37  goal thy 
    2.38 - "!!evs. [| A ~: lost;  B ~: lost;  evs : otway |]                         \
    2.39 -\        ==> Says Server B                                                 \
    2.40 -\             {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},            \
    2.41 -\               Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}           \
    2.42 -\            : set evs -->                                                 \
    2.43 -\            Says B Spy {|NA, NB, Key K|} ~: set evs -->                   \
    2.44 + "!!evs. [| A ~: lost;  B ~: lost;  evs : otway |]                 \
    2.45 +\        ==> Says Server B                                         \
    2.46 +\             {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
    2.47 +\               Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
    2.48 +\            : set evs -->                                         \
    2.49 +\            Says B Spy {|NA, NB, Key K|} ~: set evs -->           \
    2.50  \            Key K ~: analz (sees Spy evs)";
    2.51  by (etac otway.induct 1);
    2.52  by analz_sees_tac;
     3.1 --- a/src/HOL/Auth/Yahalom.ML	Tue Jul 22 11:23:03 1997 +0200
     3.2 +++ b/src/HOL/Auth/Yahalom.ML	Tue Jul 22 11:26:02 1997 +0200
     3.3 @@ -278,8 +278,8 @@
     3.4  (*B knows, by the first part of A's message, that the Server distributed 
     3.5    the key for A and B.  But this part says nothing about nonces.*)
     3.6  goal thy 
     3.7 - "!!evs. [| Crypt (shrK B) {|Agent A, Key K|} : parts (sees Spy evs); \
     3.8 -\           B ~: lost;  evs : yahalom |]                           \
     3.9 + "!!evs. [| Crypt (shrK B) {|Agent A, Key K|} : parts (sees Spy evs);   \
    3.10 +\           B ~: lost;  evs : yahalom |]                                \
    3.11  \        ==> EX NA NB. Says Server A                                    \
    3.12  \                        {|Crypt (shrK A) {|Agent B, Key K,             \
    3.13  \                                           Nonce NA, Nonce NB|},       \
    3.14 @@ -299,10 +299,10 @@
    3.15   "!!evs. evs : yahalom                                             \
    3.16  \        ==> Nonce NB ~: analz (sees Spy evs) -->                  \
    3.17  \            Crypt K (Nonce NB) : parts (sees Spy evs) -->         \
    3.18 -\            (EX A B NA. Says Server A                                  \
    3.19 -\                        {|Crypt (shrK A) {|Agent B, Key K,             \
    3.20 -\                                  Nonce NA, Nonce NB|},                \
    3.21 -\                          Crypt (shrK B) {|Agent A, Key K|}|}          \
    3.22 +\            (EX A B NA. Says Server A                             \
    3.23 +\                        {|Crypt (shrK A) {|Agent B, Key K,        \
    3.24 +\                                  Nonce NA, Nonce NB|},           \
    3.25 +\                          Crypt (shrK B) {|Agent A, Key K|}|}     \
    3.26  \                       : set evs)";
    3.27  by (parts_induct_tac 1);
    3.28  (*YM3 & Fake*)