New version of axiom sees1_Says:
authorpaulson
Wed Oct 09 13:43:51 1996 +0200 (1996-10-09)
changeset 2078b198b3d46fb4
parent 2077 477e80fe0e9b
child 2079 8f0d199373a3
New version of axiom sees1_Says:
Previously it only allowed the SENDER to see the content of messages...
Now instead the RECIPIENT sees the messages. This change had no effect
on subsequent proofs because protocol rules refer specifically to the
relevant messages sent to an agent.
src/HOL/Auth/Shared.ML
src/HOL/Auth/Shared.thy
     1.1 --- a/src/HOL/Auth/Shared.ML	Wed Oct 09 13:39:25 1996 +0200
     1.2 +++ b/src/HOL/Auth/Shared.ML	Wed Oct 09 13:43:51 1996 +0200
     1.3 @@ -125,17 +125,17 @@
     1.4  
     1.5  (** Specialized rewrite rules for (sees lost A (Says...#evs)) **)
     1.6  
     1.7 -goal thy "sees lost A (Says A B X # evs) = insert X (sees lost A evs)";
     1.8 +goal thy "sees lost B (Says A B X # evs) = insert X (sees lost B evs)";
     1.9  by (Simp_tac 1);
    1.10  qed "sees_own";
    1.11  
    1.12 -goal thy "!!A. Server ~= A ==> \
    1.13 -\              sees lost Server (Says A B X # evs) = sees lost Server evs";
    1.14 +goal thy "!!A. Server ~= B ==> \
    1.15 +\          sees lost Server (Says A B X # evs) = sees lost Server evs";
    1.16  by (Asm_simp_tac 1);
    1.17  qed "sees_Server";
    1.18  
    1.19 -goal thy "!!A. Friend i ~= A ==> \
    1.20 -\              sees lost (Friend i) (Says A B X # evs) = sees lost (Friend i) evs";
    1.21 +goal thy "!!A. Friend i ~= B ==> \
    1.22 +\          sees lost (Friend i) (Says A B X # evs) = sees lost (Friend i) evs";
    1.23  by (Asm_simp_tac 1);
    1.24  qed "sees_Friend";
    1.25  
    1.26 @@ -169,8 +169,7 @@
    1.27  qed_spec_mp "Says_imp_sees_Spy";
    1.28  
    1.29  goal thy  
    1.30 - "!!evs. [| Says A B (Crypt X (shrK C)) : set_of_list evs;        \
    1.31 -\           C   : lost |]                                         \
    1.32 + "!!evs. [| Says A B (Crypt X (shrK C)) : set_of_list evs;  C : lost |] \
    1.33  \        ==> X : analz (sees lost Spy evs)";
    1.34  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
    1.35                        addss (!simpset)) 1);
    1.36 @@ -190,8 +189,7 @@
    1.37  qed "initState_subset";
    1.38  
    1.39  goal thy "X : sees lost C evs --> \
    1.40 -\          (EX A B. Says A B X : set_of_list evs) | \
    1.41 -\          (EX A. X = Key (shrK A))";
    1.42 +\          (EX A B. Says A B X : set_of_list evs) | (EX A. X = Key (shrK A))";
    1.43  by (list.induct_tac "evs" 1);
    1.44  by (ALLGOALS Asm_simp_tac);
    1.45  by (fast_tac (!claset addDs [impOfSubs initState_subset]) 1);
     2.1 --- a/src/HOL/Auth/Shared.thy	Wed Oct 09 13:39:25 1996 +0200
     2.2 +++ b/src/HOL/Auth/Shared.thy	Wed Oct 09 13:43:51 1996 +0200
     2.3 @@ -33,10 +33,8 @@
     2.4    sees1 :: [agent, event] => msg set
     2.5  
     2.6  primrec sees1 event
     2.7 -           (*First agent recalls all that it says, but NOT everything
     2.8 -             that is sent to it; it must note such things if/when received*)
     2.9 -  sees1_Says  "sees1 A (Says A' B X)  = (if A:{A',Spy} then {X} else {})"
    2.10 -          (*part of A's internal state*)
    2.11 +           (*Spy reads all traffic whether addressed to him or not*)
    2.12 +  sees1_Says  "sees1 A (Says A' B X)  = (if A:{B,Spy} then {X} else {})"
    2.13  
    2.14  consts  
    2.15    sees :: [agent set, agent, event list] => msg set