equal
deleted
inserted
replaced
|
1 theory Send |
|
2 imports Main |
|
3 begin |
|
4 |
|
5 typedecl principal |
|
6 |
|
7 consts A :: principal |
|
8 consts S :: principal |
|
9 consts B :: principal |
|
10 |
|
11 consts Says :: "principal \<Rightarrow> bool \<Rightarrow> bool" ("_ says _") |
|
12 consts Sends :: "principal \<Rightarrow> principal \<Rightarrow> bool \<Rightarrow> bool" ("_ sends _ : _") |
|
13 consts Enc :: "bool \<Rightarrow> bool \<Rightarrow> bool" |
|
14 consts CAB :: "bool" |
|
15 consts KAB :: "bool" |
|
16 consts KAS :: "bool" |
|
17 consts KBS :: "bool" |
|
18 consts M :: "bool" |
|
19 |
|
20 axiomatization where |
|
21 saysI[intro]: "F \<Longrightarrow> P says F" and |
|
22 saysE[elim]: "\<lbrakk>P says (F1 \<longrightarrow> F2); P says F1\<rbrakk> \<Longrightarrow> P says F2" and |
|
23 says_encI[intro]: "\<lbrakk>P says F1; P says F2\<rbrakk> \<Longrightarrow> P says (Enc F1 F2)" and |
|
24 says_encE[elim]: "\<lbrakk>P says (Enc F1 F2); P says F2\<rbrakk> \<Longrightarrow> P says F1" and |
|
25 sendsE[elim]: "\<lbrakk>P sends Q : F; P says F\<rbrakk> \<Longrightarrow> Q says F" |
|
26 |
|
27 lemma |
|
28 assumes start: "A says CAB" |
|
29 and msg1: "A sends S : CAB" |
|
30 and serv1: "S says (CAB \<longrightarrow> Enc KAB KAS)" |
|
31 and serv2: "S says (CAB \<longrightarrow> Enc (Enc KAB KBS) KAS)" |
|
32 and msg2a: "S sends A : (Enc KAB KAS)" |
|
33 and msg2b: "S sends A : (Enc (Enc KAB KBS) KAS)" |
|
34 and msg3: "A sends B : (Enc KAB KBS)" |
|
35 and msg4: "A sends B : (Enc M KAB)" |
|
36 and keyA: "A says KAS" |
|
37 and keyB: "B says KBS" |
|
38 and keyS: "S says KAS" |
|
39 and MA: "A says (Enc M KAB)" |
|
40 shows "S says M" |
|
41 using assms |
|
42 |
|
43 by (metis saysE says_encE sendsE) |
|
44 |
|
45 by (metis saysE says_encE sendsE) |
|
46 |
|
47 by metis |
|
48 |
|
49 |
|
50 |
|
51 by (metis saysE says_encE sendsE) |
|
52 |
|
53 by (metis saysE says_encE sendsE) |
|
54 |
|
55 end |