author | nipkow |
Fri, 24 Nov 2000 16:49:27 +0100 | |
changeset 10519 | ade64af4c57c |
parent 5434 | 9b4bed3f394c |
child 11185 | 1b737b4c2108 |
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 |
|
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset
|
11 |
(*End marker for message bundles*) |
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset
|
12 |
syntax END :: msg |
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset
|
13 |
translations "END" == "Number 0" |
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset
|
14 |
|
2449 | 15 |
(*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
|
16 |
who receives one. |
2449 | 17 |
Perhaps the two session keys could be bundled into a single message. |
18 |
*) |
|
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
19 |
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
|
20 |
inductive "respond evs" (*Server's response to the nested message*) |
2449 | 21 |
intrs |
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset
|
22 |
One "[| Key KAB ~: used evs |] |
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset
|
23 |
==> (Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, END|}, |
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset
|
24 |
{|Crypt (shrK A) {|Key KAB, Agent B, Nonce NA|}, END|}, |
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
25 |
KAB) : respond evs" |
2449 | 26 |
|
2532 | 27 |
(*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
|
28 |
Cons "[| (PA, RA, KAB) : respond evs; |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
29 |
Key KBC ~: used evs; Key KBC ~: parts {RA}; |
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset
|
30 |
PA = Hash[Key(shrK A)] {|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
|
31 |
==> (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|}, |
2550
8d8344bcf98a
Re-ordering of certificates so that session keys appear in decreasing order
paulson
parents:
2532
diff
changeset
|
32 |
{|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, |
8d8344bcf98a
Re-ordering of certificates so that session keys appear in decreasing order
paulson
parents:
2532
diff
changeset
|
33 |
Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, |
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
34 |
RA|}, |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
35 |
KBC) |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
36 |
: respond evs" |
2449 | 37 |
|
38 |
||
2481 | 39 |
(*Induction over "respond" can be difficult due to the complexity of the |
2532 | 40 |
subgoals. Set "responses" captures the general form of certificates. |
2449 | 41 |
*) |
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
42 |
consts responses :: event list => msg set |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
43 |
inductive "responses evs" |
2449 | 44 |
intrs |
45 |
(*Server terminates lists*) |
|
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset
|
46 |
Nil "END : responses evs" |
2449 | 47 |
|
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
48 |
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
|
49 |
==> {|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
|
50 |
RA|} : responses evs" |
2449 | 51 |
|
52 |
||
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset
|
53 |
consts recur :: event list set |
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset
|
54 |
inductive "recur" |
2449 | 55 |
intrs |
56 |
(*Initial trace is empty*) |
|
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset
|
57 |
Nil "[]: recur" |
2449 | 58 |
|
2532 | 59 |
(*The spy MAY say anything he CAN say. Common to |
2449 | 60 |
all similar protocols.*) |
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset
|
61 |
Fake "[| evs: recur; X: synth (analz (spies evs)) |] |
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset
|
62 |
==> Says Spy B X # evs : recur" |
2449 | 63 |
|
64 |
(*Alice initiates a protocol run. |
|
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset
|
65 |
END is a placeholder to terminate the nesting.*) |
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset
|
66 |
RA1 "[| evs1: recur; Nonce NA ~: used evs1 |] |
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset
|
67 |
==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, END|}) |
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset
|
68 |
# evs1 : recur" |
2449 | 69 |
|
70 |
(*Bob's response to Alice's message. C might be the Server. |
|
4552
bb8ff763c93d
Simplified proofs by omitting PA = {|XA, ...|} from RA2
paulson
parents:
3683
diff
changeset
|
71 |
We omit PA = {|XA, Agent A, Agent B, Nonce NA, P|} because |
bb8ff763c93d
Simplified proofs by omitting PA = {|XA, ...|} from RA2
paulson
parents:
3683
diff
changeset
|
72 |
it complicates proofs, so B may respond to any message at all!*) |
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset
|
73 |
RA2 "[| evs2: recur; Nonce NB ~: used evs2; |
4552
bb8ff763c93d
Simplified proofs by omitting PA = {|XA, ...|} from RA2
paulson
parents:
3683
diff
changeset
|
74 |
Says A' B PA : set evs2 |] |
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset
|
75 |
==> Says B C (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|}) |
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset
|
76 |
# evs2 : recur" |
2449 | 77 |
|
2550
8d8344bcf98a
Re-ordering of certificates so that session keys appear in decreasing order
paulson
parents:
2532
diff
changeset
|
78 |
(*The Server receives Bob's message and prepares a response.*) |
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset
|
79 |
RA3 "[| evs3: recur; Says B' Server PB : set evs3; |
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset
|
80 |
(PB,RB,K) : respond evs3 |] |
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset
|
81 |
==> Says Server B RB # evs3 : recur" |
2449 | 82 |
|
83 |
(*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
|
84 |
those in the message he previously sent the Server.*) |
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset
|
85 |
RA4 "[| evs4: recur; |
2449 | 86 |
Says B C {|XH, Agent B, Agent C, Nonce NB, |
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset
|
87 |
XA, Agent A, Agent B, Nonce NA, P|} : set evs4; |
2550
8d8344bcf98a
Re-ordering of certificates so that session keys appear in decreasing order
paulson
parents:
2532
diff
changeset
|
88 |
Says C' B {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, |
8d8344bcf98a
Re-ordering of certificates so that session keys appear in decreasing order
paulson
parents:
2532
diff
changeset
|
89 |
Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, |
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset
|
90 |
RA|} : set evs4 |] |
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset
|
91 |
==> Says B A RA # evs4 : recur" |
2449 | 92 |
|
93 |
end |
|
5359 | 94 |
|
95 |
(*No "oops" message can easily be expressed. Each session key is |
|
96 |
associated--in two separate messages--with two nonces. This is |
|
97 |
one try, but it isn't that useful. Re domino attack, note that |
|
98 |
Recur.ML proves that each session key is secure provided the two |
|
99 |
peers are, even if there are compromised agents elsewhere in |
|
100 |
the chain. Oops cases proved using parts_cut, Key_in_keysFor_parts, |
|
101 |
etc. |
|
102 |
||
103 |
Oops "[| evso: recur; Says Server B RB : set evso; |
|
104 |
RB : responses evs'; Key K : parts {RB} |] |
|
105 |
==> Notes Spy {|Key K, RB|} # evso : recur" |
|
106 |
*) |