author  paulson 
Fri, 05 Sep 1997 12:24:13 +0200  
changeset 3659  eddedfe2f3f8 
parent 3519  ab0a9fbed4c0 
child 3683  aafe719dff14 
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 

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}, 
2550
8d8344bcf98a
Reordering of certificates so that session keys appear in decreasing order
paulson
parents:
2532
diff
changeset

30 
{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

31 
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

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 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

51 
consts recur :: event list set 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

52 
inductive "recur" 
2449  53 
intrs 
54 
(*Initial trace is empty*) 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

55 
Nil "[]: recur" 
2449  56 

2532  57 
(*The spy MAY say anything he CAN say. Common to 
2449  58 
all similar protocols.*) 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

59 
Fake "[ evs: recur; B ~= Spy; 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

60 
X: synth (analz (sees Spy evs)) ] 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3466
diff
changeset

61 
==> Says Spy B X # evs : recur" 
2449  62 

63 
(*Alice initiates a protocol run. 

64 
"Agent Server" is just a placeholder, to terminate the nesting.*) 

3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

65 
RA1 "[ evs1: recur; A ~= B; A ~= Server; Nonce NA ~: used evs1 ] 
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}) 
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

69 
# evs1 : recur" 
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.*) 
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

77 
RA2 "[ evs2: recur; B ~= C; B ~= Server; Nonce NB ~: used evs2; 
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

78 
Says A' B PA : set evs2; 
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}) 
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

81 
# evs2 : recur" 
2449  82 

2550
8d8344bcf98a
Reordering of certificates so that session keys appear in decreasing order
paulson
parents:
2532
diff
changeset

83 
(*The Server receives Bob's message and prepares a response.*) 
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

84 
RA3 "[ evs3: recur; B ~= Server; 
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

85 
Says B' Server PB : set evs3; 
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

86 
(PB,RB,K) : respond evs3 ] 
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

87 
==> Says Server B RB # evs3 : recur" 
2449  88 

89 
(*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

90 
those in the message he previously sent the Server.*) 
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

91 
RA4 "[ evs4: recur; A ~= B; 
2449  92 
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

93 
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

94 
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

95 
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

96 
RA} : set evs4 ] 
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

97 
==> Says B A RA # evs4 : recur" 
2449  98 

3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

99 
(**No "oops" message can easily be expressed. Each session key is 
2449  100 
associatedin two separate messageswith two nonces. 
101 
***) 

102 
end 