author | paulson |
Tue, 07 Jan 1997 10:19:43 +0100 | |
changeset 2481 | ee461c8bc9c3 |
parent 2451 | ce85a2aafc7a |
child 2485 | c4368c967c56 |
permissions | -rw-r--r-- |
2449 | 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 |
||
2481 | 9 |
Recur = HPair + Shared + |
2449 | 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 |
||
2481 | 26 |
One "A ~= Server |
27 |
==> (j, HPair (Key(shrK A)) |
|
28 |
{|Agent A, Agent B, Nonce NA, Agent Server|}, |
|
2449 | 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; |
|
2481 | 36 |
PA = HPair (Key(shrK A)) {|Agent A, Agent B, Nonce NA, P|}; |
37 |
B ~= Server |] |
|
38 |
==> (j, HPair (Key(shrK B)) {|Agent B, Agent C, Nonce NB, PA|}, |
|
2449 | 39 |
{|Agent B, |
40 |
Crypt (shrK B) {|Key(newK2(i,Suc j)), Agent A, Nonce NB|}, |
|
41 |
Agent B, |
|
42 |
Crypt (shrK B) {|Key(newK2(i,j)), Agent C, Nonce NB|}, |
|
43 |
RA|}) |
|
44 |
: respond i" |
|
45 |
||
46 |
||
2481 | 47 |
(*Induction over "respond" can be difficult due to the complexity of the |
2449 | 48 |
subgoals. The "responses" relation formalizes the general form of its |
49 |
third component. |
|
50 |
*) |
|
51 |
consts responses :: nat => msg set |
|
52 |
inductive "responses i" |
|
53 |
intrs |
|
54 |
(*Server terminates lists*) |
|
55 |
Nil "Agent Server : responses i" |
|
56 |
||
57 |
Cons "RA : responses i |
|
58 |
==> {|Agent B, |
|
59 |
Crypt (shrK B) {|Key(newK2(i,k)), Agent A, Nonce NB|}, |
|
60 |
RA|} : responses i" |
|
61 |
||
62 |
||
63 |
consts recur :: agent set => event list set |
|
64 |
inductive "recur lost" |
|
65 |
intrs |
|
66 |
(*Initial trace is empty*) |
|
67 |
Nil "[]: recur lost" |
|
68 |
||
69 |
(*The spy MAY say anything he CAN say. We do not expect him to |
|
70 |
invent new nonces here, but he can also use NS1. Common to |
|
71 |
all similar protocols.*) |
|
72 |
Fake "[| evs: recur lost; B ~= Spy; |
|
73 |
X: synth (analz (sees lost Spy evs)) |] |
|
74 |
==> Says Spy B X # evs : recur lost" |
|
75 |
||
76 |
(*Alice initiates a protocol run. |
|
77 |
"Agent Server" is just a placeholder, to terminate the nesting.*) |
|
2481 | 78 |
RA1 "[| evs: recur lost; A ~= B; A ~= Server |] |
79 |
==> Says A B |
|
80 |
(HPair (Key(shrK A)) |
|
81 |
{|Agent A, Agent B, Nonce(newN(length evs)), Agent Server|}) |
|
82 |
# evs : recur lost" |
|
2449 | 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.*) |
|
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset
|
88 |
RA2 "[| evs: recur lost; B ~= C; B ~= Server; |
2449 | 89 |
Says A' B PA : set_of_list evs; |
2481 | 90 |
PA = {|XA, Agent A, Agent B, Nonce NA, P|} |] |
91 |
==> Says B C |
|
92 |
(HPair (Key(shrK B)) |
|
93 |
{|Agent B, Agent C, Nonce (newN(length evs)), PA|}) |
|
94 |
# evs : recur lost" |
|
2449 | 95 |
|
96 |
(*The Server receives and decodes Bob's message. Then he generates |
|
97 |
a new session key and a response.*) |
|
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset
|
98 |
RA3 "[| evs: recur lost; B ~= Server; |
2449 | 99 |
Says B' Server PB : set_of_list evs; |
100 |
(0,PB,RB) : respond (length evs) |] |
|
101 |
==> Says Server B RB # evs : recur lost" |
|
102 |
||
103 |
(*Bob receives the returned message and compares the Nonces with |
|
104 |
those in the message he previously sent the Server.*) |
|
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset
|
105 |
RA4 "[| evs: recur lost; A ~= B; |
2449 | 106 |
Says C' B {|Agent B, |
107 |
Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, |
|
108 |
Agent B, |
|
109 |
Crypt (shrK B) {|Key KAC, Agent C, Nonce NB|}, RA|} |
|
110 |
: set_of_list evs; |
|
111 |
Says B C {|XH, Agent B, Agent C, Nonce NB, |
|
112 |
XA, Agent A, Agent B, Nonce NA, P|} |
|
113 |
: set_of_list evs |] |
|
114 |
==> Says B A RA # evs : recur lost" |
|
115 |
||
116 |
(**No "oops" message can readily be expressed, since each session key is |
|
117 |
associated--in two separate messages--with two nonces. |
|
118 |
***) |
|
119 |
end |