(* 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"
(*The most recent session key is passed up to the caller*)
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 KBC, Agent C, Nonce NB|},
Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
RA|},
KBC)
: respond evs"
(*Induction over "respond" can be difficult due to the complexity of the
subgoals. Set "responses" captures the general form of certificates.
*)
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. 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 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 Bob's message and prepares a response.*)
RA3 "[| evs: recur lost; B ~= Server;
Says B' Server PB : set 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 B C {|XH, Agent B, Agent C, Nonce NB,
XA, Agent A, Agent B, Nonce NA, P|}
: set evs;
Says C' B {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|},
Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
RA|}
: set 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