(* Title: HOL/Auth/Recur
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
Inductive relation "recur" for the Recursive Authentication protocol.
*)
Recur = Shared +
(*Two session keys are distributed to each agent except for the initiator,
who receives one.
Perhaps the two session keys could be bundled into a single message.
*)
consts respond :: "event list => (msg*msg*key)set"
inductive "respond evs" (*Server's response to the nested message*)
intrs
(*The message "Agent Server" marks the end of a list.*)
One "[| A ~= Server; Key KAB ~: used evs |]
==> (Hash[Key(shrK A)]
{|Agent A, Agent B, Nonce NA, Agent Server|},
{|Crypt (shrK A) {|Key KAB, Agent B, Nonce NA|}, Agent Server|},
KAB) : respond evs"
(*newK2(i,Suc j) is the key for A & B; newK2(i,j) is the key for B & C*)
Cons "[| (PA, RA, KAB) : respond evs;
Key KBC ~: used evs; Key KBC ~: parts {RA};
PA = Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, P|};
B ~= Server |]
==> (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|},
{|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|},
RA|},
KBC)
: respond evs"
(*Induction over "respond" can be difficult due to the complexity of the
subgoals. The "responses" relation formalizes the general form of its
third component.
*)
consts responses :: event list => msg set
inductive "responses evs"
intrs
(*Server terminates lists*)
Nil "Agent Server : responses evs"
Cons "[| RA : responses evs; Key KAB ~: used evs |]
==> {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
RA|} : responses evs"
consts recur :: agent set => event list set
inductive "recur lost"
intrs
(*Initial trace is empty*)
Nil "[]: recur lost"
(*The spy MAY say anything he CAN say. We do not expect him to
invent new nonces here, but he can also use NS1. Common to
all similar protocols.*)
Fake "[| evs: recur lost; B ~= Spy;
X: synth (analz (sees lost Spy evs)) |]
==> Says Spy B X # evs : recur lost"
(*Alice initiates a protocol run.
"Agent Server" is just a placeholder, to terminate the nesting.*)
RA1 "[| evs: recur lost; A ~= B; A ~= Server; Nonce NA ~: used evs |]
==> Says A B
(Hash[Key(shrK A)]
{|Agent A, Agent B, Nonce NA, Agent Server|})
# evs : recur lost"
(*Bob's response to Alice's message. C might be the Server.
XA should be the Hash of the remaining components with KA, but
Bob cannot check that.
P is the previous recur message from Alice's caller.
NOTE: existing proofs don't need PA and are complicated by its
presence! See parts_Fake_tac.*)
RA2 "[| evs: recur lost; B ~= C; B ~= Server; Nonce NB ~: used evs;
Says A' B PA : set_of_list evs;
PA = {|XA, Agent A, Agent B, Nonce NA, P|} |]
==> Says B C (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|})
# evs : recur lost"
(*The Server receives and decodes Bob's message. Then he generates
a new session key and a response.*)
RA3 "[| evs: recur lost; B ~= Server;
Says B' Server PB : set_of_list evs;
(PB,RB,K) : respond evs |]
==> Says Server B RB # evs : recur lost"
(*Bob receives the returned message and compares the Nonces with
those in the message he previously sent the Server.*)
RA4 "[| evs: recur lost; A ~= B;
Says C' B {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, RA|}
: set_of_list evs;
Says B C {|XH, Agent B, Agent C, Nonce NB,
XA, Agent A, Agent B, Nonce NA, P|}
: set_of_list evs |]
==> Says B A RA # evs : recur lost"
(**No "oops" message can readily be expressed, since each session key is
associated--in two separate messages--with two nonces.
***)
end