A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
the tactic has also changed and allows the abstaction over fuction occurences whose type is nat or int.
(* Title: HOL/Auth/Message
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
Datatypes of agents and messages;
Inductive relations "parts", "analz" and "synth"
*)
theory Message = Main
files ("Message_lemmas.ML"):
(*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
lemma [simp] : "A Un (B Un A) = B Un A"
by blast
types
key = nat
consts
invKey :: "key=>key"
axioms
invKey [simp] : "invKey (invKey K) = K"
(*The inverse of a symmetric key is itself;
that of a public key is the private key and vice versa*)
constdefs
symKeys :: "key set"
"symKeys == {K. invKey K = K}"
datatype (*We allow any number of friendly agents*)
agent = Server | Friend nat | Spy
datatype
msg = Agent agent (*Agent names*)
| Number nat (*Ordinary integers, timestamps, ...*)
| Nonce nat (*Unguessable nonces*)
| Key key (*Crypto keys*)
| Hash msg (*Hashing*)
| MPair msg msg (*Compound messages*)
| Crypt key msg (*Encryption, public- or shared-key*)
(*Concrete syntax: messages appear as {|A,B,NA|}, etc...*)
syntax
"@MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})")
syntax (xsymbols)
"@MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
translations
"{|x, y, z|}" == "{|x, {|y, z|}|}"
"{|x, y|}" == "MPair x y"
constdefs
(*Message Y, paired with a MAC computed with the help of X*)
HPair :: "[msg,msg] => msg" ("(4Hash[_] /_)" [0, 1000])
"Hash[X] Y == {| Hash{|X,Y|}, Y|}"
(*Keys useful to decrypt elements of a message set*)
keysFor :: "msg set => key set"
"keysFor H == invKey ` {K. \<exists>X. Crypt K X \<in> H}"
(** Inductive definition of all "parts" of a message. **)
consts parts :: "msg set => msg set"
inductive "parts H"
intros
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"
(*Monotonicity*)
lemma parts_mono: "G<=H ==> parts(G) <= parts(H)"
apply auto
apply (erule parts.induct)
apply (auto dest: Fst Snd Body)
done
(** 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 analz :: "msg set => msg set"
inductive "analz H"
intros
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]:
"[|Crypt K X \<in> analz H; Key(invKey K) \<in> analz H|] ==> X \<in> analz H"
(*Monotonicity; Lemma 1 of Lowe's paper*)
lemma analz_mono: "G<=H ==> analz(G) <= analz(H)"
apply auto
apply (erule analz.induct)
apply (auto dest: Fst Snd)
done
(** 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 are public domain.
Numbers can be guessed, but Nonces cannot be. **)
consts synth :: "msg set => msg set"
inductive "synth H"
intros
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"
(*Monotonicity*)
lemma synth_mono: "G<=H ==> synth(G) <= synth(H)"
apply auto
apply (erule synth.induct)
apply (auto dest: Fst Snd Body)
done
(*NO Agent_synth, as any Agent name can be synthesized. Ditto for Number*)
inductive_cases Nonce_synth [elim!]: "Nonce n \<in> synth H"
inductive_cases Key_synth [elim!]: "Key K \<in> synth H"
inductive_cases Hash_synth [elim!]: "Hash X \<in> synth H"
inductive_cases MPair_synth [elim!]: "{|X,Y|} \<in> synth H"
inductive_cases Crypt_synth [elim!]: "Crypt K X \<in> synth H"
use "Message_lemmas.ML"
lemma Fake_parts_insert_in_Un:
"[|Z \<in> parts (insert X H); X: synth (analz H)|]
==> Z \<in> synth (analz H) \<union> parts H";
by (blast dest: Fake_parts_insert [THEN subsetD, dest])
method_setup spy_analz = {*
Method.no_args (Method.METHOD (fn facts => spy_analz_tac 1)) *}
"for proving the Fake case when analz is involved"
end