src/HOL/Auth/Message.thy
changeset 1913 2809adb15eb0
parent 1839 199243afac2b
child 1947 f19a801a2bca
     1.1 --- a/src/HOL/Auth/Message.thy	Mon Aug 19 11:19:16 1996 +0200
     1.2 +++ b/src/HOL/Auth/Message.thy	Mon Aug 19 11:19:55 1996 +0200
     1.3 @@ -4,7 +4,7 @@
     1.4      Copyright   1996  University of Cambridge
     1.5  
     1.6  Datatypes of agents and messages;
     1.7 -Inductive relations "parts", "analyze" and "synthesize"
     1.8 +Inductive relations "parts", "analz" and "synth"
     1.9  *)
    1.10  
    1.11  Message = Arith +
    1.12 @@ -77,38 +77,29 @@
    1.13      Body    "Crypt X K : parts H ==> X : parts H"
    1.14  
    1.15  
    1.16 -(** Inductive definition of "analyze" -- what can be broken down from a set of
    1.17 +(** Inductive definition of "analz" -- what can be broken down from a set of
    1.18      messages, including keys.  A form of downward closure.  Pairs can
    1.19      be taken apart; messages decrypted with known keys.  **)
    1.20  
    1.21 -consts  analyze   :: msg set => msg set
    1.22 -inductive "analyze H"
    1.23 +consts  analz   :: msg set => msg set
    1.24 +inductive "analz H"
    1.25    intrs 
    1.26 -    Inj     "X: H ==> X: analyze H"
    1.27 -
    1.28 -    Fst     "{|X,Y|} : analyze H ==> X : analyze H"
    1.29 -
    1.30 -    Snd     "{|X,Y|} : analyze H ==> Y : analyze H"
    1.31 -
    1.32 -    Decrypt "[| Crypt X K : analyze H; Key(invKey K): analyze H
    1.33 -             |] ==> X : analyze H"
    1.34 +    Inj     "X: H ==> X: analz H"
    1.35 +    Fst     "{|X,Y|} : analz H ==> X : analz H"
    1.36 +    Snd     "{|X,Y|} : analz H ==> Y : analz H"
    1.37 +    Decrypt "[| Crypt X K : analz H; Key(invKey K): analz H |] ==> X : analz H"
    1.38  
    1.39  
    1.40 -(** Inductive definition of "synthesize" -- what can be built up from a set of
    1.41 +(** Inductive definition of "synth" -- what can be built up from a set of
    1.42      messages.  A form of upward closure.  Pairs can be built, messages
    1.43      encrypted with known keys.  Agent names may be quoted.  **)
    1.44  
    1.45 -consts  synthesize   :: msg set => msg set
    1.46 -inductive "synthesize H"
    1.47 +consts  synth   :: msg set => msg set
    1.48 +inductive "synth H"
    1.49    intrs 
    1.50 -    Inj     "X: H ==> X: synthesize H"
    1.51 -
    1.52 -    Agent   "Agent agt : synthesize H"
    1.53 -
    1.54 -    MPair   "[| X: synthesize H;  Y: synthesize H
    1.55 -             |] ==> {|X,Y|} : synthesize H"
    1.56 -
    1.57 -    Crypt   "[| X: synthesize H; Key(K): synthesize H
    1.58 -             |] ==> Crypt X K : synthesize H"
    1.59 +    Inj     "X: H ==> X: synth H"
    1.60 +    Agent   "Agent agt : synth H"
    1.61 +    MPair   "[| X: synth H;  Y: synth H |] ==> {|X,Y|} : synth H"
    1.62 +    Crypt   "[| X: synth H; Key(K): synth H |] ==> Crypt X K : synth H"
    1.63  
    1.64  end