src/HOL/Auth/Message.thy

changeset 1913 | 2809adb15eb0 |

parent 1839 | 199243afac2b |

child 1947 | f19a801a2bca |

--- a/src/HOL/Auth/Message.thy Mon Aug 19 11:19:16 1996 +0200 +++ b/src/HOL/Auth/Message.thy Mon Aug 19 11:19:55 1996 +0200 @@ -4,7 +4,7 @@ Copyright 1996 University of Cambridge Datatypes of agents and messages; -Inductive relations "parts", "analyze" and "synthesize" +Inductive relations "parts", "analz" and "synth" *) Message = Arith + @@ -77,38 +77,29 @@ Body "Crypt X K : parts H ==> X : parts H" -(** Inductive definition of "analyze" -- what can be broken down from a set of +(** Inductive definition of "analz" -- what can be broken down from a set of messages, including keys. A form of downward closure. Pairs can be taken apart; messages decrypted with known keys. **) -consts analyze :: msg set => msg set -inductive "analyze H" +consts analz :: msg set => msg set +inductive "analz H" intrs - Inj "X: H ==> X: analyze H" - - Fst "{|X,Y|} : analyze H ==> X : analyze H" - - Snd "{|X,Y|} : analyze H ==> Y : analyze H" - - Decrypt "[| Crypt X K : analyze H; Key(invKey K): analyze H - |] ==> X : analyze H" + 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" -(** Inductive definition of "synthesize" -- what can be built up from a set of +(** Inductive definition of "synth" -- what can be built up from a set of messages. A form of upward closure. Pairs can be built, messages encrypted with known keys. Agent names may be quoted. **) -consts synthesize :: msg set => msg set -inductive "synthesize H" +consts synth :: msg set => msg set +inductive "synth H" intrs - Inj "X: H ==> X: synthesize H" - - Agent "Agent agt : synthesize H" - - MPair "[| X: synthesize H; Y: synthesize H - |] ==> {|X,Y|} : synthesize H" - - Crypt "[| X: synthesize H; Key(K): synthesize H - |] ==> Crypt X K : synthesize H" + 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): synth H |] ==> Crypt X K : synth H" end