src/HOL/Auth/Yahalom.thy
changeset 1995 c80e58e78d9c
parent 1985 84cf16192e03
child 2032 1bbf1bdcaf56
     1.1 --- a/src/HOL/Auth/Yahalom.thy	Fri Sep 13 13:15:48 1996 +0200
     1.2 +++ b/src/HOL/Auth/Yahalom.thy	Fri Sep 13 13:16:57 1996 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      HOL/Auth/OtwayRees
     1.5 +(*  Title:      HOL/Auth/Yahalom
     1.6      ID:         $Id$
     1.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8      Copyright   1996  University of Cambridge
     1.9 @@ -10,7 +10,7 @@
    1.10    Proc. Royal Soc. 426 (1989)
    1.11  *)
    1.12  
    1.13 -OtwayRees = Shared + 
    1.14 +Yahalom = Shared + 
    1.15  
    1.16  consts  yahalom   :: "event list set"
    1.17  inductive yahalom
    1.18 @@ -26,13 +26,12 @@
    1.19  
    1.20           (*Alice initiates a protocol run*)
    1.21      YM1  "[| evs: yahalom;  A ~= B |]
    1.22 -          ==> Says A B {|Nonce (newN evs), Agent A |} # evs : yahalom"
    1.23 +          ==> Says A B {|Agent A, Nonce (newN evs)|} # evs : yahalom"
    1.24  
    1.25           (*Bob's response to Alice's message.  Bob doesn't know who 
    1.26 -	   the sender is, hence the A' in the sender field.
    1.27 -           We modify the published protocol by NOT encrypting NB.*)
    1.28 +	   the sender is, hence the A' in the sender field.*)
    1.29      YM2  "[| evs: yahalom;  B ~= Server;
    1.30 -             Says A' B {|Nonce NA, Agent A|} : set_of_list evs |]
    1.31 +             Says A' B {|Agent A, Nonce NA|} : set_of_list evs |]
    1.32            ==> Says B Server 
    1.33                    {|Agent B, 
    1.34                      Crypt {|Agent A, Nonce NA, Nonce (newN evs)|} (shrK B)|}
    1.35 @@ -40,34 +39,23 @@
    1.36  
    1.37           (*The Server receives Bob's message.  He responds by sending a
    1.38              new session key to Alice, with a packet for forwarding to Bob.*)
    1.39 -    YM3  "[| evs: yahalom;  B ~= Server;
    1.40 +    YM3  "[| evs: yahalom;  A ~= Server;
    1.41               Says B' Server 
    1.42 -                  {|Nonce NA, Agent A, Agent B, 
    1.43 -                    Crypt {|Nonce NA, Agent A, Agent B|} (shrK A), 
    1.44 -                    Nonce NB, 
    1.45 -                    Crypt {|Nonce NA, Agent A, Agent B|} (shrK B)|}
    1.46 +                  {|Agent B, Crypt {|Agent A, Nonce NA, Nonce NB|} (shrK B)|}
    1.47                 : set_of_list evs |]
    1.48 -          ==> Says Server B 
    1.49 -                  {|Nonce NA, 
    1.50 -                    Crypt {|Nonce NA, Key (newK evs)|} (shrK A),
    1.51 -                    Crypt {|Nonce NB, Key (newK evs)|} (shrK B)|}
    1.52 +          ==> Says Server A
    1.53 +                  {|Crypt {|Agent B, Key (newK evs), 
    1.54 +                            Nonce NA, Nonce NB|} (shrK A),
    1.55 +                    Crypt {|Agent A, Key (newK evs)|} (shrK B)|}
    1.56                   # evs : yahalom"
    1.57  
    1.58 -         (*Bob receives the Server's (?) message and compares the Nonces with
    1.59 -	   those in the message he previously sent the Server.*)
    1.60 +         (*Alice receives the Server's (?) message, checks her Nonce, and
    1.61 +           uses the new session key to send Bob his Nonce.*)
    1.62      YM4  "[| evs: yahalom;  A ~= B;  
    1.63 -             Says S B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|}
    1.64 +             Says S A {|Crypt {|Agent B, Key K, Nonce NA, Nonce NB|} (shrK A),
    1.65 +                        X|}
    1.66                 : set_of_list evs;
    1.67 -             Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|}
    1.68 -               : set_of_list evs |]
    1.69 -          ==> (Says B A {|Nonce NA, X|}) # evs : yahalom"
    1.70 -
    1.71 -         (*Alice checks her Nonce, then sends a dummy message to Bob,
    1.72 -           using the new session key.*)
    1.73 -    YM5  "[| evs: yahalom;  
    1.74 -             Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|}
    1.75 -               : set_of_list evs;
    1.76 -             Says A  B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |]
    1.77 -          ==> Says A B (Crypt (Agent A) K)  # evs : yahalom"
    1.78 +             Says A B {|Agent A, Nonce NA|} : set_of_list evs |]
    1.79 +          ==> Says A B {|X, Crypt (Nonce NB) K|} # evs : yahalom"
    1.80  
    1.81  end