--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/programs/Send.thy	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,55 @@
+theory Send
+imports Main
+begin
+
+typedecl principal
+
+consts A :: principal
+consts S :: principal
+consts B :: principal
+
+consts Says :: "principal \<Rightarrow> bool \<Rightarrow> bool" ("_ says _")
+consts Sends :: "principal \<Rightarrow> principal \<Rightarrow> bool \<Rightarrow> bool" ("_ sends _ : _")
+consts Enc :: "bool \<Rightarrow> bool \<Rightarrow> bool"
+consts CAB :: "bool"
+consts KAB :: "bool"
+consts KAS :: "bool" 
+consts KBS :: "bool"
+consts M :: "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: "A says CAB"
+  and     msg1:  "A sends S : CAB"
+  and    serv1:  "S says (CAB \<longrightarrow> Enc KAB KAS)"
+  and    serv2:  "S says (CAB \<longrightarrow> Enc (Enc KAB KBS) KAS)"
+  and    msg2a:  "S sends A : (Enc KAB KAS)"
+  and    msg2b:  "S sends A : (Enc (Enc KAB KBS) KAS)"
+  and     msg3:  "A sends B : (Enc KAB KBS)"
+  and     msg4:  "A sends B : (Enc M KAB)"
+  and     keyA:  "A says KAS"
+  and     keyB:  "B says KBS"
+  and     keyS:  "S says KAS"
+  and       MA:  "A says (Enc M KAB)"
+  shows "S says M"
+using assms
+
+by (metis saysE says_encE sendsE)
+
+by (metis saysE says_encE sendsE)
+
+by metis
+
+
+
+by (metis saysE says_encE sendsE)
+
+by (metis saysE says_encE sendsE)
+
+end