src/HOL/Auth/Message.thy
changeset 2284 80ebd1a213fd
parent 2121 7e118eb32bdc
child 2373 490ffa16952e
     1.1 --- a/src/HOL/Auth/Message.thy	Fri Nov 29 17:58:18 1996 +0100
     1.2 +++ b/src/HOL/Auth/Message.thy	Fri Nov 29 18:03:21 1996 +0100
     1.3 @@ -28,10 +28,10 @@
     1.4    isSymKey :: key=>bool
     1.5    "isSymKey K == (invKey K = K)"
     1.6  
     1.7 -  (*We do not assume  Crypt (Crypt X K) (invKey K) = X
     1.8 -    because Crypt is a constructor!  We assume that encryption is injective,
     1.9 +  (*We do not assume  Crypt (invKey K) (Crypt K X) = X
    1.10 +    because Crypt a is constructor!  We assume that encryption is injective,
    1.11      which is not true in the real world.  The alternative is to take
    1.12 -    Crypt as an uninterpreted function symbol satisfying the equation
    1.13 +    Crypt an as uninterpreted function symbol satisfying the equation
    1.14      above.  This seems to require moving to ZF and regarding msg as an
    1.15      inductive definition instead of a datatype.*) 
    1.16  
    1.17 @@ -43,7 +43,7 @@
    1.18        | Nonce nat
    1.19        | Key   key
    1.20        | MPair msg msg
    1.21 -      | Crypt msg key
    1.22 +      | Crypt key msg
    1.23  
    1.24  (*Allows messages of the form {|A,B,NA|}, etc...*)
    1.25  syntax
    1.26 @@ -56,7 +56,7 @@
    1.27  
    1.28  constdefs  (*Keys useful to decrypt elements of a message set*)
    1.29    keysFor :: msg set => key set
    1.30 -  "keysFor H == invKey `` {K. EX X. Crypt X K : H}"
    1.31 +  "keysFor H == invKey `` {K. EX X. Crypt K X : H}"
    1.32  
    1.33  (** Inductive definition of all "parts" of a message.  **)
    1.34  
    1.35 @@ -66,7 +66,7 @@
    1.36      Inj     "X: H ==> X: parts H"
    1.37      Fst     "{|X,Y|} : parts H ==> X : parts H"
    1.38      Snd     "{|X,Y|} : parts H ==> Y : parts H"
    1.39 -    Body    "Crypt X K : parts H ==> X : parts H"
    1.40 +    Body    "Crypt K X : parts H ==> X : parts H"
    1.41  
    1.42  
    1.43  (** Inductive definition of "analz" -- what can be broken down from a set of
    1.44 @@ -79,7 +79,7 @@
    1.45      Inj     "X: H ==> X: analz H"
    1.46      Fst     "{|X,Y|} : analz H ==> X : analz H"
    1.47      Snd     "{|X,Y|} : analz H ==> Y : analz H"
    1.48 -    Decrypt "[| Crypt X K : analz H; Key(invKey K): analz H |] ==> X : analz H"
    1.49 +    Decrypt "[| Crypt K X : analz H; Key(invKey K): analz H |] ==> X : analz H"
    1.50  
    1.51  
    1.52  (** Inductive definition of "synth" -- what can be built up from a set of
    1.53 @@ -92,6 +92,6 @@
    1.54      Inj     "X: H ==> X: synth H"
    1.55      Agent   "Agent agt : synth H"
    1.56      MPair   "[| X: synth H;  Y: synth H |] ==> {|X,Y|} : synth H"
    1.57 -    Crypt   "[| X: synth H; Key(K): H |] ==> Crypt X K : synth H"
    1.58 +    Crypt   "[| X: synth H; Key(K): H |] ==> Crypt K X : synth H"
    1.59  
    1.60  end