diff -r 6e11c7bfb9c7 -r ab0a9fbed4c0 src/HOL/Auth/Recur.thy --- a/src/HOL/Auth/Recur.thy Mon Jul 14 12:44:09 1997 +0200 +++ b/src/HOL/Auth/Recur.thy Mon Jul 14 12:47:21 1997 +0200 @@ -48,25 +48,25 @@ RA|} : responses evs" -consts recur :: agent set => event list set -inductive "recur lost" +consts recur :: event list set +inductive "recur" intrs (*Initial trace is empty*) - Nil "[]: recur lost" + Nil "[]: recur" (*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" + Fake "[| evs: recur; B ~= Spy; + X: synth (analz (sees Spy evs)) |] + ==> Says Spy B X # evs : recur" (*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 |] + RA1 "[| evs: recur; 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" + # evs : recur" (*Bob's response to Alice's message. C might be the Server. XA should be the Hash of the remaining components with KA, but @@ -74,27 +74,27 @@ 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; + RA2 "[| evs: recur; 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" + # evs : recur" (*The Server receives Bob's message and prepares a response.*) - RA3 "[| evs: recur lost; B ~= Server; + RA3 "[| evs: recur; B ~= Server; Says B' Server PB : set evs; (PB,RB,K) : respond evs |] - ==> Says Server B RB # evs : recur lost" + ==> Says Server B RB # evs : recur" (*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; + RA4 "[| evs: recur; 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" + ==> Says B A RA # evs : recur" (**No "oops" message can easily be expressed. Each session key is associated--in two separate messages--with two nonces.