src/HOL/Auth/Yahalom2.thy
changeset 6335 7e4bffaa2a3e
parent 5434 9b4bed3f394c
child 11185 1b737b4c2108
     1.1 --- a/src/HOL/Auth/Yahalom2.thy	Wed Mar 10 10:42:40 1999 +0100
     1.2 +++ b/src/HOL/Auth/Yahalom2.thy	Wed Mar 10 10:42:57 1999 +0100
     1.3 @@ -24,17 +24,21 @@
     1.4           (*The spy MAY say anything he CAN say.  We do not expect him to
     1.5             invent new nonces here, but he can also use NS1.  Common to
     1.6             all similar protocols.*)
     1.7 -    Fake "[| evs: yahalom;  X: synth (analz (spies evs)) |]
     1.8 +    Fake "[| evs: yahalom;  X: synth (analz (knows Spy evs)) |]
     1.9            ==> Says Spy B X  # evs : yahalom"
    1.10  
    1.11 +         (*A message that has been sent can be received by the
    1.12 +           intended recipient.*)
    1.13 +    Reception "[| evsr: yahalom;  Says A B X : set evsr |]
    1.14 +               ==> Gets B X # evsr : yahalom"
    1.15 +
    1.16           (*Alice initiates a protocol run*)
    1.17      YM1  "[| evs1: yahalom;  Nonce NA ~: used evs1 |]
    1.18            ==> Says A B {|Agent A, Nonce NA|} # evs1 : yahalom"
    1.19  
    1.20 -         (*Bob's response to Alice's message.  Bob doesn't know who 
    1.21 -	   the sender is, hence the A' in the sender field.*)
    1.22 +         (*Bob's response to Alice's message.*)
    1.23      YM2  "[| evs2: yahalom;  Nonce NB ~: used evs2;
    1.24 -             Says A' B {|Agent A, Nonce NA|} : set evs2 |]
    1.25 +             Gets B {|Agent A, Nonce NA|} : set evs2 |]
    1.26            ==> Says B Server 
    1.27                    {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
    1.28                  # evs2 : yahalom"
    1.29 @@ -43,8 +47,8 @@
    1.30             new session key to Alice, with a certificate for forwarding to Bob.
    1.31             Both agents are quoted in the 2nd certificate to prevent attacks!*)
    1.32      YM3  "[| evs3: yahalom;  Key KAB ~: used evs3;
    1.33 -             Says B' Server {|Agent B, Nonce NB,
    1.34 -			      Crypt (shrK B) {|Agent A, Nonce NA|}|}
    1.35 +             Gets Server {|Agent B, Nonce NB,
    1.36 +			   Crypt (shrK B) {|Agent A, Nonce NA|}|}
    1.37                 : set evs3 |]
    1.38            ==> Says Server A
    1.39                 {|Nonce NB, 
    1.40 @@ -55,8 +59,8 @@
    1.41           (*Alice receives the Server's (?) message, checks her Nonce, and
    1.42             uses the new session key to send Bob his Nonce.*)
    1.43      YM4  "[| evs4: yahalom;  
    1.44 -             Says S A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
    1.45 -                        X|}  : set evs4;
    1.46 +             Gets A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
    1.47 +                      X|}  : set evs4;
    1.48               Says A B {|Agent A, Nonce NA|} : set evs4 |]
    1.49            ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 : yahalom"
    1.50