diff -r 68829cf138fc -r 80ebd1a213fd src/HOL/Auth/Message.thy --- a/src/HOL/Auth/Message.thy Fri Nov 29 17:58:18 1996 +0100 +++ b/src/HOL/Auth/Message.thy Fri Nov 29 18:03:21 1996 +0100 @@ -28,10 +28,10 @@ isSymKey :: key=>bool "isSymKey K == (invKey K = K)" - (*We do not assume Crypt (Crypt X K) (invKey K) = X - because Crypt is a constructor! We assume that encryption is injective, + (*We do not assume Crypt (invKey K) (Crypt K X) = X + because Crypt a is constructor! We assume that encryption is injective, which is not true in the real world. The alternative is to take - Crypt as an uninterpreted function symbol satisfying the equation + Crypt an as uninterpreted function symbol satisfying the equation above. This seems to require moving to ZF and regarding msg as an inductive definition instead of a datatype.*) @@ -43,7 +43,7 @@ | Nonce nat | Key key | MPair msg msg - | Crypt msg key + | Crypt key msg (*Allows messages of the form {|A,B,NA|}, etc...*) syntax @@ -56,7 +56,7 @@ constdefs (*Keys useful to decrypt elements of a message set*) keysFor :: msg set => key set - "keysFor H == invKey `` {K. EX X. Crypt X K : H}" + "keysFor H == invKey `` {K. EX X. Crypt K X : H}" (** Inductive definition of all "parts" of a message. **) @@ -66,7 +66,7 @@ Inj "X: H ==> X: parts H" Fst "{|X,Y|} : parts H ==> X : parts H" Snd "{|X,Y|} : parts H ==> Y : parts H" - Body "Crypt X K : parts H ==> X : parts H" + Body "Crypt K X : parts H ==> X : parts H" (** Inductive definition of "analz" -- what can be broken down from a set of @@ -79,7 +79,7 @@ Inj "X: H ==> X: analz H" Fst "{|X,Y|} : analz H ==> X : analz H" Snd "{|X,Y|} : analz H ==> Y : analz H" - Decrypt "[| Crypt X K : analz H; Key(invKey K): analz H |] ==> X : analz H" + Decrypt "[| Crypt K X : analz H; Key(invKey K): analz H |] ==> X : analz H" (** Inductive definition of "synth" -- what can be built up from a set of @@ -92,6 +92,6 @@ Inj "X: H ==> X: synth H" Agent "Agent agt : synth H" MPair "[| X: synth H; Y: synth H |] ==> {|X,Y|} : synth H" - Crypt "[| X: synth H; Key(K): H |] ==> Crypt X K : synth H" + Crypt "[| X: synth H; Key(K): H |] ==> Crypt K X : synth H" end