src/HOL/Auth/Yahalom.thy
changeset 3519 ab0a9fbed4c0
parent 3481 256f38c01b98
child 3659 eddedfe2f3f8
     1.1 --- a/src/HOL/Auth/Yahalom.thy	Mon Jul 14 12:44:09 1997 +0200
     1.2 +++ b/src/HOL/Auth/Yahalom.thy	Mon Jul 14 12:47:21 1997 +0200
     1.3 @@ -12,58 +12,58 @@
     1.4  
     1.5  Yahalom = Shared + 
     1.6  
     1.7 -consts  yahalom   :: agent set => event list set
     1.8 -inductive "yahalom lost"
     1.9 +consts  yahalom   :: event list set
    1.10 +inductive "yahalom"
    1.11    intrs 
    1.12           (*Initial trace is empty*)
    1.13 -    Nil  "[]: yahalom lost"
    1.14 +    Nil  "[]: yahalom"
    1.15  
    1.16           (*The spy MAY say anything he CAN say.  We do not expect him to
    1.17             invent new nonces here, but he can also use NS1.  Common to
    1.18             all similar protocols.*)
    1.19 -    Fake "[| evs: yahalom lost;  B ~= Spy;  
    1.20 -             X: synth (analz (sees lost Spy evs)) |]
    1.21 -          ==> Says Spy B X  # evs : yahalom lost"
    1.22 +    Fake "[| evs: yahalom;  B ~= Spy;  
    1.23 +             X: synth (analz (sees Spy evs)) |]
    1.24 +          ==> Says Spy B X  # evs : yahalom"
    1.25  
    1.26           (*Alice initiates a protocol run*)
    1.27 -    YM1  "[| evs: yahalom lost;  A ~= B;  Nonce NA ~: used evs |]
    1.28 -          ==> Says A B {|Agent A, Nonce NA|} # evs : yahalom lost"
    1.29 +    YM1  "[| evs: yahalom;  A ~= B;  Nonce NA ~: used evs |]
    1.30 +          ==> Says A B {|Agent A, Nonce NA|} # evs : yahalom"
    1.31  
    1.32           (*Bob's response to Alice's message.  Bob doesn't know who 
    1.33  	   the sender is, hence the A' in the sender field.*)
    1.34 -    YM2  "[| evs: yahalom lost;  B ~= Server;  Nonce NB ~: used evs;
    1.35 +    YM2  "[| evs: yahalom;  B ~= Server;  Nonce NB ~: used evs;
    1.36               Says A' B {|Agent A, Nonce NA|} : set evs |]
    1.37            ==> Says B Server 
    1.38                    {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
    1.39 -                # evs : yahalom lost"
    1.40 +                # evs : yahalom"
    1.41  
    1.42           (*The Server receives Bob's message.  He responds by sending a
    1.43              new session key to Alice, with a packet for forwarding to Bob.*)
    1.44 -    YM3  "[| evs: yahalom lost;  A ~= Server;  Key KAB ~: used evs;
    1.45 +    YM3  "[| evs: yahalom;  A ~= Server;  Key KAB ~: used evs;
    1.46               Says B' Server 
    1.47                    {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
    1.48                 : set evs |]
    1.49            ==> Says Server A
    1.50                     {|Crypt (shrK A) {|Agent B, Key KAB, Nonce NA, Nonce NB|},
    1.51                       Crypt (shrK B) {|Agent A, Key KAB|}|}
    1.52 -                # evs : yahalom lost"
    1.53 +                # evs : yahalom"
    1.54  
    1.55           (*Alice receives the Server's (?) message, checks her Nonce, and
    1.56             uses the new session key to send Bob his Nonce.*)
    1.57 -    YM4  "[| evs: yahalom lost;  A ~= Server;  
    1.58 +    YM4  "[| evs: yahalom;  A ~= Server;  
    1.59               Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|},
    1.60                          X|}  : set evs;
    1.61               Says A B {|Agent A, Nonce NA|} : set evs |]
    1.62 -          ==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom lost"
    1.63 +          ==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom"
    1.64  
    1.65           (*This message models possible leaks of session keys.  The Nonces
    1.66             identify the protocol run.  Quoting Server here ensures they are
    1.67             correct.*)
    1.68 -    Oops "[| evs: yahalom lost;  A ~= Spy;
    1.69 +    Oops "[| evs: yahalom;  A ~= Spy;
    1.70               Says Server A {|Crypt (shrK A)
    1.71                                     {|Agent B, Key K, Nonce NA, Nonce NB|},
    1.72                               X|}  : set evs |]
    1.73 -          ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom lost"
    1.74 +          ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom"
    1.75  
    1.76  
    1.77  constdefs