20 where |
20 where |
21 |
21 |
22 Nil: "[]\<in> orb" |
22 Nil: "[]\<in> orb" |
23 |
23 |
24 | Fake: "\<lbrakk>evsa\<in> orb; X\<in> synth (analz (knows Spy evsa))\<rbrakk> |
24 | Fake: "\<lbrakk>evsa\<in> orb; X\<in> synth (analz (knows Spy evsa))\<rbrakk> |
25 \<Longrightarrow> Says Spy B X # evsa \<in> orb" |
25 \<Longrightarrow> Says Spy B X # evsa \<in> orb" |
26 |
26 |
27 | Reception: "\<lbrakk>evsr\<in> orb; Says A B X \<in> set evsr\<rbrakk> |
27 | Reception: "\<lbrakk>evsr\<in> orb; Says A B X \<in> set evsr\<rbrakk> |
28 \<Longrightarrow> Gets B X # evsr \<in> orb" |
28 \<Longrightarrow> Gets B X # evsr \<in> orb" |
29 |
29 |
30 | OR1: "\<lbrakk>evs1\<in> orb; Nonce NA \<notin> used evs1\<rbrakk> |
30 | OR1: "\<lbrakk>evs1\<in> orb; Nonce NA \<notin> used evs1\<rbrakk> |
31 \<Longrightarrow> Says A B \<lbrace>Nonce M, Agent A, Agent B, |
31 \<Longrightarrow> Says A B \<lbrace>Nonce M, Agent A, Agent B, |
32 Crypt (shrK A) \<lbrace>Nonce NA, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> |
32 Crypt (shrK A) \<lbrace>Nonce NA, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> |
33 # evs1 \<in> orb" |
33 # evs1 \<in> orb" |
34 |
34 |
35 | OR2: "\<lbrakk>evs2\<in> orb; Nonce NB \<notin> used evs2; |
35 | OR2: "\<lbrakk>evs2\<in> orb; Nonce NB \<notin> used evs2; |
36 Gets B \<lbrace>Nonce M, Agent A, Agent B, X\<rbrace> \<in> set evs2\<rbrakk> |
36 Gets B \<lbrace>Nonce M, Agent A, Agent B, X\<rbrace> \<in> set evs2\<rbrakk> |
37 \<Longrightarrow> Says B Server |
37 \<Longrightarrow> Says B Server |
38 \<lbrace>Nonce M, Agent A, Agent B, X, |
38 \<lbrace>Nonce M, Agent A, Agent B, X, |
39 Crypt (shrK B) \<lbrace>Nonce NB, Nonce M, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> |
39 Crypt (shrK B) \<lbrace>Nonce NB, Nonce M, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> |
40 # evs2 \<in> orb" |
40 # evs2 \<in> orb" |
41 |
41 |
42 | OR3: "\<lbrakk>evs3\<in> orb; Key KAB \<notin> used evs3; |
42 | OR3: "\<lbrakk>evs3\<in> orb; Key KAB \<notin> used evs3; |
43 Gets Server |
43 Gets Server |
44 \<lbrace>Nonce M, Agent A, Agent B, |
44 \<lbrace>Nonce M, Agent A, Agent B, |
45 Crypt (shrK A) \<lbrace>Nonce NA, Nonce M, Agent A, Agent B\<rbrace>, |
45 Crypt (shrK A) \<lbrace>Nonce NA, Nonce M, Agent A, Agent B\<rbrace>, |
46 Crypt (shrK B) \<lbrace>Nonce NB, Nonce M, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> |
46 Crypt (shrK B) \<lbrace>Nonce NB, Nonce M, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> |
47 \<in> set evs3\<rbrakk> |
47 \<in> set evs3\<rbrakk> |
48 \<Longrightarrow> Says Server B \<lbrace>Nonce M, |
48 \<Longrightarrow> Says Server B \<lbrace>Nonce M, |
49 Crypt (shrK B) \<lbrace>Crypt (shrK A) \<lbrace>Nonce NA, Key KAB\<rbrace>, |
49 Crypt (shrK B) \<lbrace>Crypt (shrK A) \<lbrace>Nonce NA, Key KAB\<rbrace>, |
50 Nonce NB, Key KAB\<rbrace>\<rbrace> |
50 Nonce NB, Key KAB\<rbrace>\<rbrace> |
51 # evs3 \<in> orb" |
51 # evs3 \<in> orb" |
52 |
52 |
53 (*B can only check that the message he is bouncing is a ciphertext*) |
53 (*B can only check that the message he is bouncing is a ciphertext*) |
54 (*Sending M back is omitted*) |
54 (*Sending M back is omitted*) |
55 | OR4: "\<lbrakk>evs4\<in> orb; B \<noteq> Server; \<forall> p q. X \<noteq> \<lbrace>p, q\<rbrace>; |
55 | OR4: "\<lbrakk>evs4\<in> orb; B \<noteq> Server; \<forall> p q. X \<noteq> \<lbrace>p, q\<rbrace>; |
56 Says B Server \<lbrace>Nonce M, Agent A, Agent B, X', |
56 Says B Server \<lbrace>Nonce M, Agent A, Agent B, X', |
57 Crypt (shrK B) \<lbrace>Nonce NB, Nonce M, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> |
57 Crypt (shrK B) \<lbrace>Nonce NB, Nonce M, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> |
58 \<in> set evs4; |
58 \<in> set evs4; |
59 Gets B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>X, Nonce NB, Key KAB\<rbrace>\<rbrace> |
59 Gets B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>X, Nonce NB, Key KAB\<rbrace>\<rbrace> |
60 \<in> set evs4\<rbrakk> |
60 \<in> set evs4\<rbrakk> |
61 \<Longrightarrow> Says B A \<lbrace>Nonce M, X\<rbrace> # evs4 \<in> orb" |
61 \<Longrightarrow> Says B A \<lbrace>Nonce M, X\<rbrace> # evs4 \<in> orb" |
62 |
62 |
63 |
63 |
64 | Oops: "\<lbrakk>evso\<in> orb; |
64 | Oops: "\<lbrakk>evso\<in> orb; |
65 Says Server B \<lbrace>Nonce M, |
65 Says Server B \<lbrace>Nonce M, |
66 Crypt (shrK B) \<lbrace>Crypt (shrK A) \<lbrace>Nonce NA, Key KAB\<rbrace>, |
66 Crypt (shrK B) \<lbrace>Crypt (shrK A) \<lbrace>Nonce NA, Key KAB\<rbrace>, |
67 Nonce NB, Key KAB\<rbrace>\<rbrace> |
67 Nonce NB, Key KAB\<rbrace>\<rbrace> |
68 \<in> set evso\<rbrakk> |
68 \<in> set evso\<rbrakk> |
69 \<Longrightarrow> Notes Spy \<lbrace>Agent A, Agent B, Nonce NA, Nonce NB, Key KAB\<rbrace> # evso |
69 \<Longrightarrow> Notes Spy \<lbrace>Agent A, Agent B, Nonce NA, Nonce NB, Key KAB\<rbrace> # evso |
70 \<in> orb" |
70 \<in> orb" |
71 |
71 |
72 |
72 |
73 |
73 |