Changed some variables of type msg to lower case (e.g. from NB to nb
authorpaulson
Fri Jul 04 17:36:41 1997 +0200 (1997-07-04)
changeset 35014ab477ffb4c6
parent 3500 0d8ad2f192d8
child 3502 ec22ba0a26ec
Changed some variables of type msg to lower case (e.g. from NB to nb
src/HOL/Auth/Yahalom.ML
src/HOL/Auth/Yahalom2.ML
     1.1 --- a/src/HOL/Auth/Yahalom.ML	Fri Jul 04 17:34:55 1997 +0200
     1.2 +++ b/src/HOL/Auth/Yahalom.ML	Fri Jul 04 17:36:41 1997 +0200
     1.3 @@ -138,7 +138,7 @@
     1.4  (*Describes the form of K when the Server sends this message.  Useful for
     1.5    Oops as well as main secrecy property.*)
     1.6  goal thy 
     1.7 - "!!evs. [| Says Server A {|Crypt (shrK A) {|Agent B, Key K, NA, NB|}, X|} \
     1.8 + "!!evs. [| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \
     1.9  \             : set evs;                                                   \
    1.10  \           evs : yahalom lost |]                                          \
    1.11  \        ==> K ~: range shrK";
    1.12 @@ -466,7 +466,7 @@
    1.13  goal thy 
    1.14   "!!evs. evs : yahalom lost ==>                                            \
    1.15  \   EX NA' A' B'. ALL NA A B.                                              \
    1.16 -\      Crypt (shrK B) {|Agent A, Nonce NA, NB|} : parts(sees lost Spy evs) \
    1.17 +\      Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts(sees lost Spy evs) \
    1.18  \      --> B ~: lost --> NA = NA' & A = A' & B = B'";
    1.19  by parts_induct_tac;
    1.20  (*Fake*)
    1.21 @@ -474,15 +474,15 @@
    1.22      THEN Fake_parts_insert_tac 1);
    1.23  by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
    1.24  (*YM2: creation of new Nonce.  Move assertion into global context*)
    1.25 -by (expand_case_tac "NB = ?y" 1);
    1.26 +by (expand_case_tac "nb = ?y" 1);
    1.27  by (REPEAT (resolve_tac [exI, conjI, impI, refl] 1));
    1.28  by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
    1.29  val lemma = result();
    1.30  
    1.31  goal thy 
    1.32 - "!!evs.[| Crypt (shrK B) {|Agent A, Nonce NA, NB|}        \
    1.33 + "!!evs.[| Crypt (shrK B) {|Agent A, Nonce NA, nb|}        \
    1.34  \                  : parts (sees lost Spy evs);            \
    1.35 -\          Crypt (shrK B') {|Agent A', Nonce NA', NB|}     \
    1.36 +\          Crypt (shrK B') {|Agent A', Nonce NA', nb|}     \
    1.37  \                  : parts (sees lost Spy evs);            \
    1.38  \          evs : yahalom lost;  B ~: lost;  B' ~: lost |]  \
    1.39  \        ==> NA' = NA & A' = A & B' = B";
    1.40 @@ -493,11 +493,11 @@
    1.41  (*Variant useful for proving secrecy of NB: the Says... form allows 
    1.42    not_lost_tac to remove the assumption B' ~: lost.*)
    1.43  goal thy 
    1.44 - "!!evs.[| Says C D   {|X,  Crypt (shrK B) {|Agent A, Nonce NA, NB|}|}    \
    1.45 + "!!evs.[| Says C D   {|X,  Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}    \
    1.46  \            : set evs;          B ~: lost;                               \
    1.47 -\          Says C' D' {|X', Crypt (shrK B') {|Agent A', Nonce NA', NB|}|} \
    1.48 +\          Says C' D' {|X', Crypt (shrK B') {|Agent A', Nonce NA', nb|}|} \
    1.49  \            : set evs;                                                   \
    1.50 -\          NB ~: analz (sees lost Spy evs);  evs : yahalom lost |]        \
    1.51 +\          nb ~: analz (sees lost Spy evs);  evs : yahalom lost |]        \
    1.52  \        ==> NA' = NA & A' = A & B' = B";
    1.53  by (not_lost_tac "B'" 1);
    1.54  by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
    1.55 @@ -513,7 +513,7 @@
    1.56  goal thy 
    1.57   "!!evs. [| B ~: lost;  evs : yahalom lost  |]       \
    1.58  \ ==> Nonce NB ~: analz (sees lost Spy evs) -->      \
    1.59 -\     Crypt (shrK B') {|Agent A', Nonce NB, NB'|}    \
    1.60 +\     Crypt (shrK B') {|Agent A', Nonce NB, nb'|}    \
    1.61  \       : parts(sees lost Spy evs)                   \
    1.62  \ --> Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|} \
    1.63  \       ~: parts(sees lost Spy evs)";
     2.1 --- a/src/HOL/Auth/Yahalom2.ML	Fri Jul 04 17:34:55 1997 +0200
     2.2 +++ b/src/HOL/Auth/Yahalom2.ML	Fri Jul 04 17:36:41 1997 +0200
     2.3 @@ -138,7 +138,7 @@
     2.4  (*Describes the form of K when the Server sends this message.  Useful for
     2.5    Oops as well as main secrecy property.*)
     2.6  goal thy 
     2.7 - "!!evs. [| Says Server A {|NB', Crypt (shrK A) {|Agent B, Key K, NA|}, X|} \
     2.8 + "!!evs. [| Says Server A {|nb', Crypt (shrK A) {|Agent B, Key K, na|}, X|} \
     2.9  \            : set evs;                                                 \
    2.10  \           evs : yahalom lost |]                                       \
    2.11  \        ==> K ~: range shrK & A ~= B";