author | paulson |
Tue, 21 Jan 1997 10:54:05 +0100 | |
changeset 2532 | cde25bf71cc1 |
parent 2516 | 4d68fbe6378b |
child 2550 | 8d8344bcf98a |
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 |
||
2485
c4368c967c56
Simplification of some proofs, especially by eliminating
paulson
parents:
2481
diff
changeset
|
9 |
Recur = Shared + |
2449 | 10 |
|
11 |
(*Two session keys are distributed to each agent except for the initiator, |
|
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
12 |
who receives one. |
2449 | 13 |
Perhaps the two session keys could be bundled into a single message. |
14 |
*) |
|
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
15 |
consts respond :: "event list => (msg*msg*key)set" |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
16 |
inductive "respond evs" (*Server's response to the nested message*) |
2449 | 17 |
intrs |
18 |
(*The message "Agent Server" marks the end of a list.*) |
|
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
19 |
One "[| A ~= Server; Key KAB ~: used evs |] |
2532 | 20 |
==> (Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, Agent Server|}, |
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
21 |
{|Crypt (shrK A) {|Key KAB, Agent B, Nonce NA|}, Agent Server|}, |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
22 |
KAB) : respond evs" |
2449 | 23 |
|
2532 | 24 |
(*The most recent session key is passed up to the caller*) |
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
25 |
Cons "[| (PA, RA, KAB) : respond evs; |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
26 |
Key KBC ~: used evs; Key KBC ~: parts {RA}; |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
27 |
PA = Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, P|}; |
2481 | 28 |
B ~= Server |] |
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
29 |
==> (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|}, |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
30 |
{|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
31 |
Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
32 |
RA|}, |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
33 |
KBC) |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
34 |
: respond evs" |
2449 | 35 |
|
36 |
||
2481 | 37 |
(*Induction over "respond" can be difficult due to the complexity of the |
2532 | 38 |
subgoals. Set "responses" captures the general form of certificates. |
2449 | 39 |
*) |
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
40 |
consts responses :: event list => msg set |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
41 |
inductive "responses evs" |
2449 | 42 |
intrs |
43 |
(*Server terminates lists*) |
|
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
44 |
Nil "Agent Server : responses evs" |
2449 | 45 |
|
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
46 |
Cons "[| RA : responses evs; Key KAB ~: used evs |] |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
47 |
==> {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
48 |
RA|} : responses evs" |
2449 | 49 |
|
50 |
||
51 |
consts recur :: agent set => event list set |
|
52 |
inductive "recur lost" |
|
53 |
intrs |
|
54 |
(*Initial trace is empty*) |
|
55 |
Nil "[]: recur lost" |
|
56 |
||
2532 | 57 |
(*The spy MAY say anything he CAN say. Common to |
2449 | 58 |
all similar protocols.*) |
59 |
Fake "[| evs: recur lost; B ~= Spy; |
|
60 |
X: synth (analz (sees lost Spy evs)) |] |
|
61 |
==> Says Spy B X # evs : recur lost" |
|
62 |
||
63 |
(*Alice initiates a protocol run. |
|
64 |
"Agent Server" is just a placeholder, to terminate the nesting.*) |
|
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
65 |
RA1 "[| evs: recur lost; A ~= B; A ~= Server; Nonce NA ~: used evs |] |
2481 | 66 |
==> Says A B |
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
67 |
(Hash[Key(shrK A)] |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
68 |
{|Agent A, Agent B, Nonce NA, Agent Server|}) |
2481 | 69 |
# evs : recur lost" |
2449 | 70 |
|
71 |
(*Bob's response to Alice's message. C might be the Server. |
|
72 |
XA should be the Hash of the remaining components with KA, but |
|
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
73 |
Bob cannot check that. |
2485
c4368c967c56
Simplification of some proofs, especially by eliminating
paulson
parents:
2481
diff
changeset
|
74 |
P is the previous recur message from Alice's caller. |
c4368c967c56
Simplification of some proofs, especially by eliminating
paulson
parents:
2481
diff
changeset
|
75 |
NOTE: existing proofs don't need PA and are complicated by its |
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
76 |
presence! See parts_Fake_tac.*) |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
77 |
RA2 "[| evs: recur lost; B ~= C; B ~= Server; Nonce NB ~: used evs; |
2449 | 78 |
Says A' B PA : set_of_list evs; |
2481 | 79 |
PA = {|XA, Agent A, Agent B, Nonce NA, P|} |] |
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
80 |
==> Says B C (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|}) |
2481 | 81 |
# evs : recur lost" |
2449 | 82 |
|
83 |
(*The Server receives and decodes Bob's message. Then he generates |
|
84 |
a new session key and a response.*) |
|
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset
|
85 |
RA3 "[| evs: recur lost; B ~= Server; |
2449 | 86 |
Says B' Server PB : set_of_list evs; |
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
87 |
(PB,RB,K) : respond evs |] |
2449 | 88 |
==> Says Server B RB # evs : recur lost" |
89 |
||
90 |
(*Bob receives the returned message and compares the Nonces with |
|
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
91 |
those in the message he previously sent the Server.*) |
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset
|
92 |
RA4 "[| evs: recur lost; A ~= B; |
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
93 |
Says C' B {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
94 |
Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, RA|} |
2449 | 95 |
: set_of_list evs; |
96 |
Says B C {|XH, Agent B, Agent C, Nonce NB, |
|
97 |
XA, Agent A, Agent B, Nonce NA, P|} |
|
98 |
: set_of_list evs |] |
|
99 |
==> Says B A RA # evs : recur lost" |
|
100 |
||
101 |
(**No "oops" message can readily be expressed, since each session key is |
|
102 |
associated--in two separate messages--with two nonces. |
|
103 |
***) |
|
104 |
end |