author  paulson 
Tue, 21 Jan 1997 10:54:05 +0100  
changeset 2532  cde25bf71cc1 
parent 2516  4d68fbe6378b 
child 2550  8d8344bcf98a 
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}, 
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 
associatedin two separate messageswith two nonces. 

103 
***) 

104 
end 