|
1 (* Title: HOL/Auth/Recur |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1996 University of Cambridge |
|
5 |
|
6 Inductive relation "recur" for the Recursive Authentication protocol. |
|
7 *) |
|
8 |
|
9 Recur = Shared + |
|
10 |
|
11 syntax |
|
12 newK2 :: "nat*nat => key" |
|
13 |
|
14 translations |
|
15 "newK2 x" == "newK(nPair x)" |
|
16 |
|
17 (*Two session keys are distributed to each agent except for the initiator, |
|
18 who receives one. |
|
19 Perhaps the two session keys could be bundled into a single message. |
|
20 *) |
|
21 consts respond :: "nat => (nat*msg*msg)set" |
|
22 inductive "respond i" (*Server's response to the nested message*) |
|
23 intrs |
|
24 (*The message "Agent Server" marks the end of a list.*) |
|
25 |
|
26 One "[| A ~= Server; |
|
27 MA = {|Agent A, Agent B, Nonce NA, Agent Server|} |] |
|
28 ==> (j, {|Hash{|Key(shrK A), MA|}, MA|}, |
|
29 {|Agent A, |
|
30 Crypt (shrK A) {|Key(newK2(i,j)), Agent B, Nonce NA|}, |
|
31 Agent Server|}) |
|
32 : respond i" |
|
33 |
|
34 (*newK2(i,Suc j) is the key for A & B; newK2(i,j) is the key for B & C*) |
|
35 Cons "[| (Suc j, PA, RA) : respond i; |
|
36 B ~= Server; |
|
37 MB = {|Agent B, Agent C, Nonce NB, PA|}; |
|
38 PA = {|Hash{|Key(shrK A), MA|}, MA|}; |
|
39 MA = {|Agent A, Agent B, Nonce NA, P|} |] |
|
40 ==> (j, {|Hash{|Key(shrK B), MB|}, MB|}, |
|
41 {|Agent B, |
|
42 Crypt (shrK B) {|Key(newK2(i,Suc j)), Agent A, Nonce NB|}, |
|
43 Agent B, |
|
44 Crypt (shrK B) {|Key(newK2(i,j)), Agent C, Nonce NB|}, |
|
45 RA|}) |
|
46 : respond i" |
|
47 |
|
48 |
|
49 (*Induction over "respond" can be difficult, due to the complexity of the |
|
50 subgoals. The "responses" relation formalizes the general form of its |
|
51 third component. |
|
52 *) |
|
53 consts responses :: nat => msg set |
|
54 inductive "responses i" |
|
55 intrs |
|
56 (*Server terminates lists*) |
|
57 Nil "Agent Server : responses i" |
|
58 |
|
59 Cons "RA : responses i |
|
60 ==> {|Agent B, |
|
61 Crypt (shrK B) {|Key(newK2(i,k)), Agent A, Nonce NB|}, |
|
62 RA|} : responses i" |
|
63 |
|
64 |
|
65 consts recur :: agent set => event list set |
|
66 inductive "recur lost" |
|
67 intrs |
|
68 (*Initial trace is empty*) |
|
69 Nil "[]: recur lost" |
|
70 |
|
71 (*The spy MAY say anything he CAN say. We do not expect him to |
|
72 invent new nonces here, but he can also use NS1. Common to |
|
73 all similar protocols.*) |
|
74 Fake "[| evs: recur lost; B ~= Spy; |
|
75 X: synth (analz (sees lost Spy evs)) |] |
|
76 ==> Says Spy B X # evs : recur lost" |
|
77 |
|
78 (*Alice initiates a protocol run. |
|
79 "Agent Server" is just a placeholder, to terminate the nesting.*) |
|
80 NA1 "[| evs: recur lost; A ~= B; A ~= Server; |
|
81 MA = {|Agent A, Agent B, Nonce(newN(length evs)), Agent Server|}|] |
|
82 ==> Says A B {|Hash{|Key(shrK A),MA|}, MA|} # evs : recur lost" |
|
83 |
|
84 (*Bob's response to Alice's message. C might be the Server. |
|
85 XA should be the Hash of the remaining components with KA, but |
|
86 Bob cannot check that. |
|
87 P is the previous recur message from Alice's caller.*) |
|
88 NA2 "[| evs: recur lost; B ~= C; B ~= Server; |
|
89 Says A' B PA : set_of_list evs; |
|
90 PA = {|XA, Agent A, Agent B, Nonce NA, P|}; |
|
91 MB = {|Agent B, Agent C, Nonce (newN(length evs)), PA|} |] |
|
92 ==> Says B C {|Hash{|Key(shrK B),MB|}, MB|} # evs : recur lost" |
|
93 |
|
94 (*The Server receives and decodes Bob's message. Then he generates |
|
95 a new session key and a response.*) |
|
96 NA3 "[| evs: recur lost; B ~= Server; |
|
97 Says B' Server PB : set_of_list evs; |
|
98 (0,PB,RB) : respond (length evs) |] |
|
99 ==> Says Server B RB # evs : recur lost" |
|
100 |
|
101 (*Bob receives the returned message and compares the Nonces with |
|
102 those in the message he previously sent the Server.*) |
|
103 NA4 "[| evs: recur lost; A ~= B; |
|
104 Says C' B {|Agent B, |
|
105 Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, |
|
106 Agent B, |
|
107 Crypt (shrK B) {|Key KAC, Agent C, Nonce NB|}, RA|} |
|
108 : set_of_list evs; |
|
109 Says B C {|XH, Agent B, Agent C, Nonce NB, |
|
110 XA, Agent A, Agent B, Nonce NA, P|} |
|
111 : set_of_list evs |] |
|
112 ==> Says B A RA # evs : recur lost" |
|
113 |
|
114 (**No "oops" message can readily be expressed, since each session key is |
|
115 associated--in two separate messages--with two nonces. |
|
116 ***) |
|
117 end |