--- a/doc-src/TutorialI/Protocol/Message.thy Wed Jul 11 10:52:20 2007 +0200
+++ b/doc-src/TutorialI/Protocol/Message.thy Wed Jul 11 10:53:39 2007 +0200
@@ -66,13 +66,14 @@
(** Inductive definition of all "parts" of a message. **)
-consts parts :: "msg set => msg set"
-inductive "parts H"
- intros
+inductive_set
+ parts :: "msg set => msg set"
+ for H :: "msg set"
+ where
Inj [intro]: "X \<in> H ==> X \<in> parts H"
- Fst: "{|X,Y|} \<in> parts H ==> X \<in> parts H"
- Snd: "{|X,Y|} \<in> parts H ==> Y \<in> parts H"
- Body: "Crypt K X \<in> parts H ==> X \<in> parts H"
+ | Fst: "{|X,Y|} \<in> parts H ==> X \<in> parts H"
+ | Snd: "{|X,Y|} \<in> parts H ==> Y \<in> parts H"
+ | Body: "Crypt K X \<in> parts H ==> X \<in> parts H"
(*Monotonicity*)
@@ -87,13 +88,14 @@
messages, including keys. A form of downward closure. Pairs can
be taken apart; messages decrypted with known keys. **)
-consts analz :: "msg set => msg set"
-inductive "analz H"
- intros
+inductive_set
+ analz :: "msg set => msg set"
+ for H :: "msg set"
+ where
Inj [intro,simp] : "X \<in> H ==> X \<in> analz H"
- Fst: "{|X,Y|} \<in> analz H ==> X \<in> analz H"
- Snd: "{|X,Y|} \<in> analz H ==> Y \<in> analz H"
- Decrypt [dest]:
+ | Fst: "{|X,Y|} \<in> analz H ==> X \<in> analz H"
+ | Snd: "{|X,Y|} \<in> analz H ==> Y \<in> analz H"
+ | Decrypt [dest]:
"[|Crypt K X \<in> analz H; Key(invKey K) \<in> analz H|] ==> X \<in> analz H"
@@ -109,15 +111,16 @@
encrypted with known keys. Agent names are public domain.
Numbers can be guessed, but Nonces cannot be. **)
-consts synth :: "msg set => msg set"
-inductive "synth H"
- intros
+inductive_set
+ synth :: "msg set => msg set"
+ for H :: "msg set"
+ where
Inj [intro]: "X \<in> H ==> X \<in> synth H"
- Agent [intro]: "Agent agt \<in> synth H"
- Number [intro]: "Number n \<in> synth H"
- Hash [intro]: "X \<in> synth H ==> Hash X \<in> synth H"
- MPair [intro]: "[|X \<in> synth H; Y \<in> synth H|] ==> {|X,Y|} \<in> synth H"
- Crypt [intro]: "[|X \<in> synth H; Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
+ | Agent [intro]: "Agent agt \<in> synth H"
+ | Number [intro]: "Number n \<in> synth H"
+ | Hash [intro]: "X \<in> synth H ==> Hash X \<in> synth H"
+ | MPair [intro]: "[|X \<in> synth H; Y \<in> synth H|] ==> {|X,Y|} \<in> synth H"
+ | Crypt [intro]: "[|X \<in> synth H; Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
(*Monotonicity*)
lemma synth_mono: "G<=H ==> synth(G) <= synth(H)"