src/HOL/Auth/Yahalom2.thy
changeset 11185 1b737b4c2108
parent 6335 7e4bffaa2a3e
child 11251 a6816d47f41d
     1.1 --- a/src/HOL/Auth/Yahalom2.thy	Tue Feb 27 12:28:42 2001 +0100
     1.2 +++ b/src/HOL/Auth/Yahalom2.thy	Tue Feb 27 16:13:23 2001 +0100
     1.3 @@ -19,58 +19,58 @@
     1.4  inductive "yahalom"
     1.5    intrs 
     1.6           (*Initial trace is empty*)
     1.7 -    Nil  "[]: yahalom"
     1.8 +    Nil  "[] \\<in> yahalom"
     1.9  
    1.10           (*The spy MAY say anything he CAN say.  We do not expect him to
    1.11             invent new nonces here, but he can also use NS1.  Common to
    1.12             all similar protocols.*)
    1.13 -    Fake "[| evs: yahalom;  X: synth (analz (knows Spy evs)) |]
    1.14 -          ==> Says Spy B X  # evs : yahalom"
    1.15 +    Fake "[| evsf \\<in> yahalom;  X \\<in> synth (analz (knows Spy evsf)) |]
    1.16 +          ==> Says Spy B X  # evsf \\<in> yahalom"
    1.17  
    1.18           (*A message that has been sent can be received by the
    1.19             intended recipient.*)
    1.20 -    Reception "[| evsr: yahalom;  Says A B X : set evsr |]
    1.21 -               ==> Gets B X # evsr : yahalom"
    1.22 +    Reception "[| evsr \\<in> yahalom;  Says A B X \\<in> set evsr |]
    1.23 +               ==> Gets B X # evsr \\<in> yahalom"
    1.24  
    1.25           (*Alice initiates a protocol run*)
    1.26 -    YM1  "[| evs1: yahalom;  Nonce NA ~: used evs1 |]
    1.27 -          ==> Says A B {|Agent A, Nonce NA|} # evs1 : yahalom"
    1.28 +    YM1  "[| evs1 \\<in> yahalom;  Nonce NA \\<notin> used evs1 |]
    1.29 +          ==> Says A B {|Agent A, Nonce NA|} # evs1 \\<in> yahalom"
    1.30  
    1.31           (*Bob's response to Alice's message.*)
    1.32 -    YM2  "[| evs2: yahalom;  Nonce NB ~: used evs2;
    1.33 -             Gets B {|Agent A, Nonce NA|} : set evs2 |]
    1.34 +    YM2  "[| evs2 \\<in> yahalom;  Nonce NB \\<notin> used evs2;
    1.35 +             Gets B {|Agent A, Nonce NA|} \\<in> set evs2 |]
    1.36            ==> Says B Server 
    1.37                    {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
    1.38 -                # evs2 : yahalom"
    1.39 +                # evs2 \\<in> yahalom"
    1.40  
    1.41           (*The Server receives Bob's message.  He responds by sending a
    1.42             new session key to Alice, with a certificate for forwarding to Bob.
    1.43             Both agents are quoted in the 2nd certificate to prevent attacks!*)
    1.44 -    YM3  "[| evs3: yahalom;  Key KAB ~: used evs3;
    1.45 +    YM3  "[| evs3 \\<in> yahalom;  Key KAB \\<notin> used evs3;
    1.46               Gets Server {|Agent B, Nonce NB,
    1.47  			   Crypt (shrK B) {|Agent A, Nonce NA|}|}
    1.48 -               : set evs3 |]
    1.49 +               \\<in> set evs3 |]
    1.50            ==> Says Server A
    1.51                 {|Nonce NB, 
    1.52                   Crypt (shrK A) {|Agent B, Key KAB, Nonce NA|},
    1.53                   Crypt (shrK B) {|Agent A, Agent B, Key KAB, Nonce NB|}|}
    1.54 -                 # evs3 : yahalom"
    1.55 +                 # evs3 \\<in> yahalom"
    1.56  
    1.57           (*Alice receives the Server's (?) message, checks her Nonce, and
    1.58             uses the new session key to send Bob his Nonce.*)
    1.59 -    YM4  "[| evs4: yahalom;  
    1.60 +    YM4  "[| evs4 \\<in> yahalom;  
    1.61               Gets A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
    1.62 -                      X|}  : set evs4;
    1.63 -             Says A B {|Agent A, Nonce NA|} : set evs4 |]
    1.64 -          ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 : yahalom"
    1.65 +                      X|}  \\<in> set evs4;
    1.66 +             Says A B {|Agent A, Nonce NA|} \\<in> set evs4 |]
    1.67 +          ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 \\<in> yahalom"
    1.68  
    1.69           (*This message models possible leaks of session keys.  The nonces
    1.70             identify the protocol run.  Quoting Server here ensures they are
    1.71             correct. *)
    1.72 -    Oops "[| evso: yahalom;  
    1.73 +    Oops "[| evso \\<in> yahalom;  
    1.74               Says Server A {|Nonce NB, 
    1.75                               Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
    1.76 -                             X|}  : set evso |]
    1.77 -          ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso : yahalom"
    1.78 +                             X|}  \\<in> set evso |]
    1.79 +          ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso \\<in> yahalom"
    1.80  
    1.81  end