diff -r 3ad2493fa0e0 -r ce85a2aafc7a src/HOL/Auth/Recur.thy --- a/src/HOL/Auth/Recur.thy Thu Dec 19 11:54:19 1996 +0100 +++ b/src/HOL/Auth/Recur.thy Thu Dec 19 11:58:39 1996 +0100 @@ -77,7 +77,7 @@ (*Alice initiates a protocol run. "Agent Server" is just a placeholder, to terminate the nesting.*) - NA1 "[| evs: recur lost; A ~= B; A ~= Server; + RA1 "[| evs: recur lost; A ~= B; A ~= Server; MA = {|Agent A, Agent B, Nonce(newN(length evs)), Agent Server|}|] ==> Says A B {|Hash{|Key(shrK A),MA|}, MA|} # evs : recur lost" @@ -85,7 +85,7 @@ 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.*) - NA2 "[| evs: recur lost; B ~= C; B ~= Server; + RA2 "[| evs: recur lost; B ~= C; B ~= Server; Says A' B PA : set_of_list evs; PA = {|XA, Agent A, Agent B, Nonce NA, P|}; MB = {|Agent B, Agent C, Nonce (newN(length evs)), PA|} |] @@ -93,14 +93,14 @@ (*The Server receives and decodes Bob's message. Then he generates a new session key and a response.*) - NA3 "[| evs: recur lost; B ~= Server; + RA3 "[| evs: recur lost; B ~= Server; Says B' Server PB : set_of_list evs; (0,PB,RB) : respond (length 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.*) - NA4 "[| evs: recur lost; A ~= B; + RA4 "[| evs: recur lost; A ~= B; Says C' B {|Agent B, Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, Agent B,