author  paulson 
Fri, 18 Oct 1996 11:39:10 +0200  
changeset 2105  782772e744dc 
parent 2064  5a5e508e2a2b 
child 2135  80477862ab33 
permissions  rwrr 
1941  1 
(* Title: HOL/Auth/OtwayRees 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1996 University of Cambridge 

5 

6 
Inductive relation "otway" for the OtwayRees protocol. 

7 

2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset

8 
Version that encrypts Nonce NB 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset

9 

1941  10 
From page 244 of 
11 
Burrows, Abadi and Needham. A Logic of Authentication. 

12 
Proc. Royal Soc. 426 (1989) 

13 
*) 

14 

15 
OtwayRees = Shared + 

16 

2032  17 
consts otway :: "agent set => event list set" 
18 
inductive "otway lost" 

1941  19 
intrs 
20 
(*Initial trace is empty*) 

2032  21 
Nil "[]: otway lost" 
1941  22 

2032  23 
(*The spy MAY say anything he CAN say. We do not expect him to 
1941  24 
invent new nonces here, but he can also use NS1. Common to 
25 
all similar protocols.*) 

2032  26 
Fake "[ evs: otway lost; B ~= Spy; 
27 
X: synth (analz (sees lost Spy evs)) ] 

28 
==> Says Spy B X # evs : otway lost" 

1941  29 

30 
(*Alice initiates a protocol run*) 

2032  31 
OR1 "[ evs: otway lost; A ~= B; B ~= Server ] 
1976  32 
==> Says A B {Nonce (newN evs), Agent A, Agent B, 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset

33 
Crypt {Nonce (newN evs), Agent A, Agent B} 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset

34 
(shrK A) } 
2032  35 
# evs : otway lost" 
1941  36 

37 
(*Bob's response to Alice's message. Bob doesn't know who 

38 
the sender is, hence the A' in the sender field. 

2105  39 
Note that NB is encrypted.*) 
2032  40 
OR2 "[ evs: otway lost; B ~= Server; 
1976  41 
Says A' B {Nonce NA, Agent A, Agent B, X} : set_of_list evs ] 
42 
==> Says B Server 

2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset

43 
{Nonce NA, Agent A, Agent B, X, 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset

44 
Crypt {Nonce NA, Nonce (newN evs), 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset

45 
Agent A, Agent B} (shrK B)} 
2032  46 
# evs : otway lost" 
1941  47 

48 
(*The Server receives Bob's message and checks that the three NAs 

49 
match. Then he sends a new session key to Bob with a packet for 

50 
forwarding to Alice.*) 

2032  51 
OR3 "[ evs: otway lost; B ~= Server; 
1941  52 
Says B' Server 
53 
{Nonce NA, Agent A, Agent B, 

54 
Crypt {Nonce NA, Agent A, Agent B} (shrK A), 

2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset

55 
Crypt {Nonce NA, Nonce NB, Agent A, Agent B} (shrK B)} 
1976  56 
: set_of_list evs ] 
57 
==> Says Server B 

1941  58 
{Nonce NA, 
59 
Crypt {Nonce NA, Key (newK evs)} (shrK A), 

60 
Crypt {Nonce NB, Key (newK evs)} (shrK B)} 

2032  61 
# evs : otway lost" 
1941  62 

63 
(*Bob receives the Server's (?) message and compares the Nonces with 

64 
those in the message he previously sent the Server.*) 

2032  65 
OR4 "[ evs: otway lost; A ~= B; B ~= Server; 
1941  66 
Says S B {Nonce NA, X, Crypt {Nonce NB, Key K} (shrK B)} 
67 
: set_of_list evs; 

2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset

68 
Says B Server {Nonce NA, Agent A, Agent B, X', 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset

69 
Crypt {Nonce NA, Nonce NB, Agent A, Agent B} 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset

70 
(shrK B)} 
1976  71 
: set_of_list evs ] 
2032  72 
==> Says B A {Nonce NA, X} # evs : otway lost" 
1941  73 

2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset

74 
(*This message models possible leaks of session keys. Alice's Nonce 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1976
diff
changeset

75 
identifies the protocol run.*) 
2064  76 
Revl "[ evs: otway lost; A ~= Spy; 
77 
Says B' A {Nonce NA, Crypt {Nonce NA, Key K} (shrK A)} 

78 
: set_of_list evs; 

79 
Says A B {Nonce NA, Agent A, Agent B, 

80 
Crypt {Nonce NA, Agent A, Agent B} (shrK A)} 

81 
: set_of_list evs ] 

82 
==> Says A Spy {Nonce NA, Key K} # evs : otway lost" 

1941  83 

84 
end 