author | Christian Urban <urbanc@in.tum.de> |
Wed, 31 May 2017 09:26:47 +0100 | |
changeset 514 | a118052cf1d4 |
parent 198 | 2ce98ee39990 |
permissions | -rw-r--r-- |
198
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
1 |
theory Engin |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
2 |
imports Main |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
3 |
begin |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
4 |
|
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
5 |
typedecl principal |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
6 |
|
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
7 |
consts E :: principal |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
8 |
consts T :: principal |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
9 |
consts M :: principal |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
10 |
|
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
11 |
consts Says :: "principal \<Rightarrow> bool \<Rightarrow> bool" ("_ says _" [101, 101] 100) |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
12 |
consts Sends :: "principal \<Rightarrow> principal \<Rightarrow> bool \<Rightarrow> bool" ("_ sends _ : _" [100, 100, 100] 100) |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
13 |
consts Enc :: "bool \<Rightarrow> bool \<Rightarrow> bool" |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
14 |
consts Id :: "principal \<Rightarrow> bool" |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
15 |
|
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
16 |
consts N :: "bool" |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
17 |
consts K :: "bool" |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
18 |
consts start_engine :: "principal \<Rightarrow> bool" |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
19 |
|
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
20 |
|
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
21 |
axiomatization where |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
22 |
saysI[intro]: "F \<Longrightarrow> P says F" and |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
23 |
saysE[elim]: "\<lbrakk>P says (F1 \<longrightarrow> F2); P says F1\<rbrakk> \<Longrightarrow> P says F2" and |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
24 |
says_encI[intro]: "\<lbrakk>P says F1; P says F2\<rbrakk> \<Longrightarrow> P says (Enc F1 F2)" and |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
25 |
says_encE[elim]: "\<lbrakk>P says (Enc F1 F2); P says F2\<rbrakk> \<Longrightarrow> P says F1" and |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
26 |
sendsE[elim]: "\<lbrakk>P sends Q : F; P says F\<rbrakk> \<Longrightarrow> Q says F" |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
27 |
|
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
28 |
|
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
29 |
lemma |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
30 |
assumes start: "E says N" |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
31 |
and challenge: "E sends T : N" |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
32 |
and response: "T says N \<longrightarrow> (T sends E : (Enc N K) \<and> T sends E : Id(T))" |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
33 |
and keyT: "T says K" |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
34 |
and idT: "T says Id T" |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
35 |
and engine: "(E says (Enc N K) \<and> E says Id(T)) \<longrightarrow> start_engine T" |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
36 |
shows "start_engine T" |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
37 |
using assms |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
38 |
by (metis says_encI sendsE) |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
39 |
|
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
40 |
lemma |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
41 |
assumes start: "E says N" |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
42 |
and challenge: "\<forall>T. E sends T : N" |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
43 |
and response: "\<forall>N E. T says N \<longrightarrow> (T sends E : (Enc N K) \<and> T sends E : Id(T))" |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
44 |
and keyT: "T says K" |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
45 |
and idT: "T says Id T" |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
46 |
and engine: "\<forall>T. (E says (Enc N K) \<and> E says Id(T)) \<longrightarrow> start_engine T" |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
47 |
shows "start_engine M" |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
48 |
using assms |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
49 |
sorry |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
50 |
(*by (metis saysE says_encE says_encI sendsE)*) |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
51 |
|
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
52 |
lemma |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
53 |
assumes start: "E says N" |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
54 |
and challenge: "\<forall>T. E sends T : N" |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
55 |
and response: "\<forall>N E. T says N \<longrightarrow> (T sends E : (Enc N K) \<and> T sends E : Id T)" |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
56 |
and keyT: "T says K" |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
57 |
and idT: "T says Id T" |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
58 |
and engine: "\<forall>T. (E says (Enc N K) \<and> E says Id T) \<longrightarrow> start_engine T" |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
59 |
and middle1: "\<forall>N. M sends T : N" |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
60 |
and middle2: "\<forall>N'. M sends E : N'" |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
61 |
and middle3: "M says Id M" |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
62 |
shows "start_engine M" |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
63 |
using assms |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
64 |
|
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
65 |
by (metis saysE says_encE says_encI sendsE) |
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
66 |
|
2ce98ee39990
reorganised
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
67 |
end |