28 constdefs |
28 constdefs |
29 "response" :: "agent => agent => nat => msg" |
29 "response" :: "agent => agent => nat => msg" |
30 "response S R q == Hash {|Agent S, Key (shrK R), Nonce q|}" |
30 "response S R q == Hash {|Agent S, Key (shrK R), Nonce q|}" |
31 |
31 |
32 |
32 |
33 consts certified_mail :: "event list set" |
33 inductive_set certified_mail :: "event list set" |
34 inductive "certified_mail" |
34 where |
35 intros |
35 |
36 |
36 Nil: --{*The empty trace*} |
37 Nil: --{*The empty trace*} |
|
38 "[] \<in> certified_mail" |
37 "[] \<in> certified_mail" |
39 |
38 |
40 Fake: --{*The Spy may say anything he can say. The sender field is correct, |
39 | Fake: --{*The Spy may say anything he can say. The sender field is correct, |
41 but agents don't use that information.*} |
40 but agents don't use that information.*} |
42 "[| evsf \<in> certified_mail; X \<in> synth(analz(spies evsf))|] |
41 "[| evsf \<in> certified_mail; X \<in> synth(analz(spies evsf))|] |
43 ==> Says Spy B X # evsf \<in> certified_mail" |
42 ==> Says Spy B X # evsf \<in> certified_mail" |
44 |
43 |
45 FakeSSL: --{*The Spy may open SSL sessions with TTP, who is the only agent |
44 | FakeSSL: --{*The Spy may open SSL sessions with TTP, who is the only agent |
46 equipped with the necessary credentials to serve as an SSL server.*} |
45 equipped with the necessary credentials to serve as an SSL server.*} |
47 "[| evsfssl \<in> certified_mail; X \<in> synth(analz(spies evsfssl))|] |
46 "[| evsfssl \<in> certified_mail; X \<in> synth(analz(spies evsfssl))|] |
48 ==> Notes TTP {|Agent Spy, Agent TTP, X|} # evsfssl \<in> certified_mail" |
47 ==> Notes TTP {|Agent Spy, Agent TTP, X|} # evsfssl \<in> certified_mail" |
49 |
48 |
50 CM1: --{*The sender approaches the recipient. The message is a number.*} |
49 | CM1: --{*The sender approaches the recipient. The message is a number.*} |
51 "[|evs1 \<in> certified_mail; |
50 "[|evs1 \<in> certified_mail; |
52 Key K \<notin> used evs1; |
51 Key K \<notin> used evs1; |
53 K \<in> symKeys; |
52 K \<in> symKeys; |
54 Nonce q \<notin> used evs1; |
53 Nonce q \<notin> used evs1; |
55 hs = Hash{|Number cleartext, Nonce q, response S R q, Crypt K (Number m)|}; |
54 hs = Hash{|Number cleartext, Nonce q, response S R q, Crypt K (Number m)|}; |
56 S2TTP = Crypt(pubEK TTP) {|Agent S, Number BothAuth, Key K, Agent R, hs|}|] |
55 S2TTP = Crypt(pubEK TTP) {|Agent S, Number BothAuth, Key K, Agent R, hs|}|] |
57 ==> Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number BothAuth, |
56 ==> Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number BothAuth, |
58 Number cleartext, Nonce q, S2TTP|} # evs1 |
57 Number cleartext, Nonce q, S2TTP|} # evs1 |
59 \<in> certified_mail" |
58 \<in> certified_mail" |
60 |
59 |
61 CM2: --{*The recipient records @{term S2TTP} while transmitting it and her |
60 | CM2: --{*The recipient records @{term S2TTP} while transmitting it and her |
62 password to @{term TTP} over an SSL channel.*} |
61 password to @{term TTP} over an SSL channel.*} |
63 "[|evs2 \<in> certified_mail; |
62 "[|evs2 \<in> certified_mail; |
64 Gets R {|Agent S, Agent TTP, em, Number BothAuth, Number cleartext, |
63 Gets R {|Agent S, Agent TTP, em, Number BothAuth, Number cleartext, |
65 Nonce q, S2TTP|} \<in> set evs2; |
64 Nonce q, S2TTP|} \<in> set evs2; |
66 TTP \<noteq> R; |
65 TTP \<noteq> R; |
67 hr = Hash {|Number cleartext, Nonce q, response S R q, em|} |] |
66 hr = Hash {|Number cleartext, Nonce q, response S R q, em|} |] |
68 ==> |
67 ==> |
69 Notes TTP {|Agent R, Agent TTP, S2TTP, Key(RPwd R), hr|} # evs2 |
68 Notes TTP {|Agent R, Agent TTP, S2TTP, Key(RPwd R), hr|} # evs2 |
70 \<in> certified_mail" |
69 \<in> certified_mail" |
71 |
70 |
72 CM3: --{*@{term TTP} simultaneously reveals the key to the recipient and gives |
71 | CM3: --{*@{term TTP} simultaneously reveals the key to the recipient and gives |
73 a receipt to the sender. The SSL channel does not authenticate |
72 a receipt to the sender. The SSL channel does not authenticate |
74 the client (@{term R}), but @{term TTP} accepts the message only |
73 the client (@{term R}), but @{term TTP} accepts the message only |
75 if the given password is that of the claimed sender, @{term R}. |
74 if the given password is that of the claimed sender, @{term R}. |
76 He replies over the established SSL channel.*} |
75 He replies over the established SSL channel.*} |
77 "[|evs3 \<in> certified_mail; |
76 "[|evs3 \<in> certified_mail; |