13 Proc. Royal Soc. 426 (1989) |
13 Proc. Royal Soc. 426 (1989) |
14 *) |
14 *) |
15 |
15 |
16 Yahalom2 = Shared + |
16 Yahalom2 = Shared + |
17 |
17 |
18 consts yahalom :: agent set => event list set |
18 consts yahalom :: event list set |
19 inductive "yahalom lost" |
19 inductive "yahalom" |
20 intrs |
20 intrs |
21 (*Initial trace is empty*) |
21 (*Initial trace is empty*) |
22 Nil "[]: yahalom lost" |
22 Nil "[]: yahalom" |
23 |
23 |
24 (*The spy MAY say anything he CAN say. We do not expect him to |
24 (*The spy MAY say anything he CAN say. We do not expect him to |
25 invent new nonces here, but he can also use NS1. Common to |
25 invent new nonces here, but he can also use NS1. Common to |
26 all similar protocols.*) |
26 all similar protocols.*) |
27 Fake "[| evs: yahalom lost; B ~= Spy; |
27 Fake "[| evs: yahalom; B ~= Spy; |
28 X: synth (analz (sees lost Spy evs)) |] |
28 X: synth (analz (sees Spy evs)) |] |
29 ==> Says Spy B X # evs : yahalom lost" |
29 ==> Says Spy B X # evs : yahalom" |
30 |
30 |
31 (*Alice initiates a protocol run*) |
31 (*Alice initiates a protocol run*) |
32 YM1 "[| evs: yahalom lost; A ~= B; Nonce NA ~: used evs |] |
32 YM1 "[| evs: yahalom; A ~= B; Nonce NA ~: used evs |] |
33 ==> Says A B {|Agent A, Nonce NA|} # evs : yahalom lost" |
33 ==> Says A B {|Agent A, Nonce NA|} # evs : yahalom" |
34 |
34 |
35 (*Bob's response to Alice's message. Bob doesn't know who |
35 (*Bob's response to Alice's message. Bob doesn't know who |
36 the sender is, hence the A' in the sender field.*) |
36 the sender is, hence the A' in the sender field.*) |
37 YM2 "[| evs: yahalom lost; B ~= Server; Nonce NB ~: used evs; |
37 YM2 "[| evs: yahalom; B ~= Server; Nonce NB ~: used evs; |
38 Says A' B {|Agent A, Nonce NA|} : set evs |] |
38 Says A' B {|Agent A, Nonce NA|} : set evs |] |
39 ==> Says B Server |
39 ==> Says B Server |
40 {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|} |
40 {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|} |
41 # evs : yahalom lost" |
41 # evs : yahalom" |
42 |
42 |
43 (*The Server receives Bob's message. He responds by sending a |
43 (*The Server receives Bob's message. He responds by sending a |
44 new session key to Alice, with a packet for forwarding to Bob. |
44 new session key to Alice, with a packet for forwarding to Bob. |
45 !! Fields are reversed in the 2nd packet to prevent attacks!! *) |
45 !! Fields are reversed in the 2nd packet to prevent attacks!! *) |
46 YM3 "[| evs: yahalom lost; A ~= B; A ~= Server; Key KAB ~: used evs; |
46 YM3 "[| evs: yahalom; A ~= B; A ~= Server; Key KAB ~: used evs; |
47 Says B' Server {|Agent B, Nonce NB, |
47 Says B' Server {|Agent B, Nonce NB, |
48 Crypt (shrK B) {|Agent A, Nonce NA|}|} |
48 Crypt (shrK B) {|Agent A, Nonce NA|}|} |
49 : set evs |] |
49 : set evs |] |
50 ==> Says Server A |
50 ==> Says Server A |
51 {|Nonce NB, |
51 {|Nonce NB, |
52 Crypt (shrK A) {|Agent B, Key KAB, Nonce NA|}, |
52 Crypt (shrK A) {|Agent B, Key KAB, Nonce NA|}, |
53 Crypt (shrK B) {|Nonce NB, Key KAB, Agent A|}|} |
53 Crypt (shrK B) {|Nonce NB, Key KAB, Agent A|}|} |
54 # evs : yahalom lost" |
54 # evs : yahalom" |
55 |
55 |
56 (*Alice receives the Server's (?) message, checks her Nonce, and |
56 (*Alice receives the Server's (?) message, checks her Nonce, and |
57 uses the new session key to send Bob his Nonce.*) |
57 uses the new session key to send Bob his Nonce.*) |
58 YM4 "[| evs: yahalom lost; A ~= Server; |
58 YM4 "[| evs: yahalom; A ~= Server; |
59 Says S A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, |
59 Says S A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, |
60 X|} : set evs; |
60 X|} : set evs; |
61 Says A B {|Agent A, Nonce NA|} : set evs |] |
61 Says A B {|Agent A, Nonce NA|} : set evs |] |
62 ==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom lost" |
62 ==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom" |
63 |
63 |
64 (*This message models possible leaks of session keys. The nonces |
64 (*This message models possible leaks of session keys. The nonces |
65 identify the protocol run. Quoting Server here ensures they are |
65 identify the protocol run. Quoting Server here ensures they are |
66 correct. *) |
66 correct. *) |
67 Oops "[| evs: yahalom lost; A ~= Spy; |
67 Oops "[| evs: yahalom; A ~= Spy; |
68 Says Server A {|Nonce NB, |
68 Says Server A {|Nonce NB, |
69 Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, |
69 Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, |
70 X|} : set evs |] |
70 X|} : set evs |] |
71 ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom lost" |
71 ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom" |
72 |
72 |
73 end |
73 end |