(* formalisation of concepts from Alwen Tiu, A trace based bisimulation for the spi-calculus: an extended abstract. In Proceedings of APLAS 2007, LNCS 4807, pages 367 - 382, 2007 *) (* Spi_General.thy,ML - general-purpose definitions and useful easy lemmas *) theory Spi_General imports WfUn dtree Pi_Gen begin datatype 'n msg = Name "'n" | Rigid nat | Mpair "'n msg" "'n msg" | Enc "'n msg" "'n msg" consts Unname :: "'n msg => 'n" primrec "Unname (Name x) = x" types 'n obs_thy = "('n msg * 'n msg) set" 'n obs_seq = "('n msg * 'n msg) srseq" datatype 'a io = In 'a | Out 'a types (* marked message pair *) 'n mmp = "('n msg * 'n msg) io" types 'n bitrace = "'n mmp list" (* in reverse order *) consts map_io :: "('a => 'b) => ('a io => 'b io)" rem_io :: "'a io => 'a" oth_of :: "'a io list => 'a set" (* eg bitrace => obs_thy *) rev_bt :: "('a * 'b) io list => ('b * 'a) io list" (* eg bitrace => obs_thy *) fst_bt :: "('a * 'b) io list => 'a io list" (* eg bitrace => obs_thy *) snd_bt :: "('a * 'b) io list => 'b io list" (* eg bitrace => obs_thy *) Ne :: "'n obs_thy" (* sorts of message *) Mpairs :: "'n msg set" Encs :: "'n msg set" Rigids :: "'n msg set" Names :: "'n => 'n msg * 'n msg" (* free names *) fnl_msg :: "'n msg => 'n list" fnl_msgs :: "'n msg * 'n msg => 'n list" fn_msg :: "'n msg => 'n set" fn_msgs :: "'n msg * 'n msg => 'n set" fn_oth :: "'n obs_thy => 'n set" fn_con :: "'n msg set * 'n msg => 'n set" fnl_bt :: "'n bitrace => 'n list" fnl_st :: "'n msg io list => 'n list" fn_bt :: "'n bitrace => 'n set list" oth_ctg_fns :: "'n set => 'n obs_thy" ms_ctg_fns :: "'n set => 'n msg set" (* property that message is atomic *) atomic_msg :: "'n msg set" (* property that keys are atomic *) ka_msg :: "'n msg set" ka_oth :: "'n obs_thy => bool" isubmsg :: "('n msg * 'n msg) set" inductive "Mpairs" intros I : "(Mpair Ma Mb) : Mpairs" inductive "Encs" intros I : "(Enc Mp Mk) : Encs" inductive "Rigids" intros I : "(Rigid a) : Rigids" inductive "Ne" intros I : "(Name i, Name i) : Ne" defs Names_def : "Names i == (Name i, Name i)" primrec "rem_io (In mp) = mp" "rem_io (Out mp) = mp" primrec "map_io f (In a) = In (f a)" "map_io f (Out a) = Out (f a)" primrec "fn_msg (Name i) = {i}" "fn_msg (Rigid i) = {}" "fn_msg (Mpair Ma Mb) = fn_msg Ma Un fn_msg Mb" "fn_msg (Enc Mp Mk) = fn_msg Mp Un fn_msg Mk" primrec "fnl_msg (Name i) = [i]" "fnl_msg (Rigid i) = []" "fnl_msg (Mpair Ma Mb) = fnl_msg Ma @ fnl_msg Mb" "fnl_msg (Enc Mp Mk) = fnl_msg Mp @ fnl_msg Mk" primrec "fn_msgs (M, N) = fn_msg M Un fn_msg N" primrec "fn_con (S, N) = (UN M:S. fn_msg M) Un fn_msg N" primrec "fnl_msgs (M, N) = fnl_msg M @ fnl_msg N" defs fn_oth_def : "fn_oth oth == UN mn:oth. fn_msgs mn" defs fnl_bt_def : "fnl_bt bt == concat (map (fnl_msgs o rem_io) bt)" fnl_st_def : "fnl_st st == concat (map (fnl_msg o rem_io) st)" rev_bt_def : "rev_bt bt == map (map_io rev_pair) bt" fst_bt_def : "fst_bt bt == map (map_io fst) bt" snd_bt_def : "snd_bt bt == map (map_io snd) bt" primrec Nil : "fn_bt [] = []" Cons : "fn_bt (mmp # mmps) = fn_msgs (rem_io mmp) # fn_bt mmps" inductive "oth_of bt" intros InI : "In MN : set bt ==> MN : oth_of bt" OutI : "Out MN : set bt ==> MN : oth_of bt" inductive "atomic_msg" intros NameI : "Name i : atomic_msg" RigidI : "Rigid i : atomic_msg" inductive "ka_msg" intros NameI : "Name i : ka_msg" RigidI : "Rigid i : ka_msg" MpairI : "Ma : ka_msg ==> Mb : ka_msg ==> (Mpair Ma Mb) : ka_msg" EncI : "Mk : atomic_msg ==> Mp : ka_msg ==> (Enc Mp Mk) : ka_msg" defs ka_oth_def : "ka_oth oth == ALL x:oth. x : ka_msg <*> ka_msg" inductive "oth_ctg_fns ns" intros I : "[| n : ns; n : fn_msgs mmp |] ==> mmp : oth_ctg_fns ns" inductive "ms_ctg_fns ns" intros I : "[| n : ns; n : fn_msg mmp |] ==> mmp : ms_ctg_fns ns" consts left :: "'n msg => 'n msg" right :: "'n msg => 'n msg" key :: "'n msg => 'n msg" plain :: "'n msg => 'n msg" primrec "key (Enc Mp Mk) = Mk" primrec "plain (Enc Mp Mk) = Mp" primrec "left (Mpair Ma Mb) = Ma" primrec "right (Mpair Ma Mb) = Mb" consts keys :: "'n msg * 'n msg => 'n msg * 'n msg" primrec "keys (M, N) = (key M, key N)" inductive "isubmsg" intros EncpI : "(Mp, Enc Mp Mk) : isubmsg" EnckI : "(Mk, Enc Mp Mk) : isubmsg" MpairaI : "(Ma, Mpair Ma Mb) : isubmsg" MpairbI : "(Mb, Mpair Ma Mb) : isubmsg" consts msg_size :: "'n msg => nat" seq_fst_size :: "'n obs_seq => nat" primrec NameI : "msg_size (Name n) = Suc 0" RigidI : "msg_size (Rigid n) = Suc 0" MpairI : "msg_size (Mpair Ma Mb) = Suc (msg_size Ma + msg_size Mb)" EncI : "msg_size (Enc Mp Mk) = Suc (msg_size Mp + msg_size Mk)" primrec seq_fst_size_def : "seq_fst_size (G, MN) = setsum (size o fst) G + size (fst MN)" (* property of deductive systems *) consts lhs_wk :: "('msg set * 'msg) set => bool" defs lhs_wk_def : "lhs_wk ders == ALL (S, M) : ders. ALL S' >= S. (S', M) : ders" (* blocker - to be proved *) consts block :: "'a set set => 'a set set" axioms block : "(EX A : AA. ALL a : A. P a) = (ALL B : block A. EX b : B. P b)" end