src/HOL/Auth/Yahalom2.thy
changeset 5434 9b4bed3f394c
parent 5359 bd539b72d484
child 6335 7e4bffaa2a3e
     1.1 --- a/src/HOL/Auth/Yahalom2.thy	Tue Sep 08 14:54:21 1998 +0200
     1.2 +++ b/src/HOL/Auth/Yahalom2.thy	Tue Sep 08 15:17:11 1998 +0200
     1.3 @@ -24,17 +24,16 @@
     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;  B ~= Spy;  
     1.8 -             X: synth (analz (spies evs)) |]
     1.9 +    Fake "[| evs: yahalom;  X: synth (analz (spies evs)) |]
    1.10            ==> Says Spy B X  # evs : yahalom"
    1.11  
    1.12           (*Alice initiates a protocol run*)
    1.13 -    YM1  "[| evs1: yahalom;  A ~= B;  Nonce NA ~: used evs1 |]
    1.14 +    YM1  "[| evs1: yahalom;  Nonce NA ~: used evs1 |]
    1.15            ==> Says A B {|Agent A, Nonce NA|} # evs1 : yahalom"
    1.16  
    1.17           (*Bob's response to Alice's message.  Bob doesn't know who 
    1.18  	   the sender is, hence the A' in the sender field.*)
    1.19 -    YM2  "[| evs2: yahalom;  B ~= Server;  Nonce NB ~: used evs2;
    1.20 +    YM2  "[| evs2: yahalom;  Nonce NB ~: used evs2;
    1.21               Says A' B {|Agent A, Nonce NA|} : set evs2 |]
    1.22            ==> Says B Server 
    1.23                    {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
    1.24 @@ -43,7 +42,7 @@
    1.25           (*The Server receives Bob's message.  He responds by sending a
    1.26             new session key to Alice, with a certificate for forwarding to Bob.
    1.27             Both agents are quoted in the 2nd certificate to prevent attacks!*)
    1.28 -    YM3  "[| evs3: yahalom;  A ~= B;  A ~= Server;  Key KAB ~: used evs3;
    1.29 +    YM3  "[| evs3: yahalom;  Key KAB ~: used evs3;
    1.30               Says B' Server {|Agent B, Nonce NB,
    1.31  			      Crypt (shrK B) {|Agent A, Nonce NA|}|}
    1.32                 : set evs3 |]
    1.33 @@ -55,7 +54,7 @@
    1.34  
    1.35           (*Alice receives the Server's (?) message, checks her Nonce, and
    1.36             uses the new session key to send Bob his Nonce.*)
    1.37 -    YM4  "[| evs4: yahalom;  A ~= Server;  
    1.38 +    YM4  "[| evs4: yahalom;  
    1.39               Says S A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
    1.40                          X|}  : set evs4;
    1.41               Says A B {|Agent A, Nonce NA|} : set evs4 |]