theory Enginimports Mainbegintypedecl principalconsts E :: principalconsts T :: principalconsts M :: principalconsts Says :: "principal \<Rightarrow> bool \<Rightarrow> bool" ("_ says _" [101, 101] 100)consts Sends :: "principal \<Rightarrow> principal \<Rightarrow> bool \<Rightarrow> bool" ("_ sends _ : _" [100, 100, 100] 100)consts Enc :: "bool \<Rightarrow> bool \<Rightarrow> bool"consts Id :: "principal \<Rightarrow> bool"consts N :: "bool"consts K :: "bool"consts start_engine :: "principal \<Rightarrow> bool"axiomatization where saysI[intro]: "F \<Longrightarrow> P says F" and saysE[elim]: "\<lbrakk>P says (F1 \<longrightarrow> F2); P says F1\<rbrakk> \<Longrightarrow> P says F2" and says_encI[intro]: "\<lbrakk>P says F1; P says F2\<rbrakk> \<Longrightarrow> P says (Enc F1 F2)" and says_encE[elim]: "\<lbrakk>P says (Enc F1 F2); P says F2\<rbrakk> \<Longrightarrow> P says F1" and sendsE[elim]: "\<lbrakk>P sends Q : F; P says F\<rbrakk> \<Longrightarrow> Q says F"lemma assumes start: "E says N" and challenge: "E sends T : N" and response: "T says N \<longrightarrow> (T sends E : (Enc N K) \<and> T sends E : Id(T))" and keyT: "T says K" and idT: "T says Id T" and engine: "(E says (Enc N K) \<and> E says Id(T)) \<longrightarrow> start_engine T" shows "start_engine T"using assmsby (metis says_encI sendsE)lemma assumes start: "E says N" and challenge: "\<forall>T. E sends T : N" and response: "\<forall>N E. T says N \<longrightarrow> (T sends E : (Enc N K) \<and> T sends E : Id(T))" and keyT: "T says K" and idT: "T says Id T" and engine: "\<forall>T. (E says (Enc N K) \<and> E says Id(T)) \<longrightarrow> start_engine T" shows "start_engine M"using assmssorry(*by (metis saysE says_encE says_encI sendsE)*)lemma assumes start: "E says N" and challenge: "\<forall>T. E sends T : N" and response: "\<forall>N E. T says N \<longrightarrow> (T sends E : (Enc N K) \<and> T sends E : Id T)" and keyT: "T says K" and idT: "T says Id T" and engine: "\<forall>T. (E says (Enc N K) \<and> E says Id T) \<longrightarrow> start_engine T" and middle1: "\<forall>N. M sends T : N" and middle2: "\<forall>N'. M sends E : N'" and middle3: "M says Id M" shows "start_engine M"using assmsby (metis saysE says_encE says_encI sendsE)end