diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/programs/Engine.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/programs/Engine.thy	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,67 @@
+theory Engin
+imports Main
+begin
+
+typedecl principal
+
+consts E :: principal
+consts T :: principal
+consts M :: principal
+
+consts 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 assms
+by (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 assms
+sorry
+(*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 assms
+
+by (metis saysE says_encE says_encI sendsE)
+
+end