author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 5434  9b4bed3f394c 
child 11185  1b737b4c2108 
permissions  rwrr 
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
Reordering 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
Reordering 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
Reordering 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
Reordering 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
Reordering 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 
associatedin two separate messageswith 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 
*) 