src/HOL/Auth/Yahalom.thy
changeset 1995 c80e58e78d9c
parent 1985 84cf16192e03
child 2032 1bbf1bdcaf56
equal deleted inserted replaced
1994:4ddfafdeefa4 1995:c80e58e78d9c
     1 (*  Title:      HOL/Auth/OtwayRees
     1 (*  Title:      HOL/Auth/Yahalom
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     4     Copyright   1996  University of Cambridge
     5 
     5 
     6 Inductive relation "yahalom" for the Yahalom protocol.
     6 Inductive relation "yahalom" for the Yahalom protocol.
     8 From page 257 of
     8 From page 257 of
     9   Burrows, Abadi and Needham.  A Logic of Authentication.
     9   Burrows, Abadi and Needham.  A Logic of Authentication.
    10   Proc. Royal Soc. 426 (1989)
    10   Proc. Royal Soc. 426 (1989)
    11 *)
    11 *)
    12 
    12 
    13 OtwayRees = Shared + 
    13 Yahalom = Shared + 
    14 
    14 
    15 consts  yahalom   :: "event list set"
    15 consts  yahalom   :: "event list set"
    16 inductive yahalom
    16 inductive yahalom
    17   intrs 
    17   intrs 
    18          (*Initial trace is empty*)
    18          (*Initial trace is empty*)
    24     Fake "[| evs: yahalom;  B ~= Enemy;  X: synth (analz (sees Enemy evs)) |]
    24     Fake "[| evs: yahalom;  B ~= Enemy;  X: synth (analz (sees Enemy evs)) |]
    25           ==> Says Enemy B X  # evs : yahalom"
    25           ==> Says Enemy B X  # evs : yahalom"
    26 
    26 
    27          (*Alice initiates a protocol run*)
    27          (*Alice initiates a protocol run*)
    28     YM1  "[| evs: yahalom;  A ~= B |]
    28     YM1  "[| evs: yahalom;  A ~= B |]
    29           ==> Says A B {|Nonce (newN evs), Agent A |} # evs : yahalom"
    29           ==> Says A B {|Agent A, Nonce (newN evs)|} # evs : yahalom"
    30 
    30 
    31          (*Bob's response to Alice's message.  Bob doesn't know who 
    31          (*Bob's response to Alice's message.  Bob doesn't know who 
    32 	   the sender is, hence the A' in the sender field.
    32 	   the sender is, hence the A' in the sender field.*)
    33            We modify the published protocol by NOT encrypting NB.*)
       
    34     YM2  "[| evs: yahalom;  B ~= Server;
    33     YM2  "[| evs: yahalom;  B ~= Server;
    35              Says A' B {|Nonce NA, Agent A|} : set_of_list evs |]
    34              Says A' B {|Agent A, Nonce NA|} : set_of_list evs |]
    36           ==> Says B Server 
    35           ==> Says B Server 
    37                   {|Agent B, 
    36                   {|Agent B, 
    38                     Crypt {|Agent A, Nonce NA, Nonce (newN evs)|} (shrK B)|}
    37                     Crypt {|Agent A, Nonce NA, Nonce (newN evs)|} (shrK B)|}
    39                  # evs : yahalom"
    38                  # evs : yahalom"
    40 
    39 
    41          (*The Server receives Bob's message.  He responds by sending a
    40          (*The Server receives Bob's message.  He responds by sending a
    42             new session key to Alice, with a packet for forwarding to Bob.*)
    41             new session key to Alice, with a packet for forwarding to Bob.*)
    43     YM3  "[| evs: yahalom;  B ~= Server;
    42     YM3  "[| evs: yahalom;  A ~= Server;
    44              Says B' Server 
    43              Says B' Server 
    45                   {|Nonce NA, Agent A, Agent B, 
    44                   {|Agent B, Crypt {|Agent A, Nonce NA, Nonce NB|} (shrK B)|}
    46                     Crypt {|Nonce NA, Agent A, Agent B|} (shrK A), 
       
    47                     Nonce NB, 
       
    48                     Crypt {|Nonce NA, Agent A, Agent B|} (shrK B)|}
       
    49                : set_of_list evs |]
    45                : set_of_list evs |]
    50           ==> Says Server B 
    46           ==> Says Server A
    51                   {|Nonce NA, 
    47                   {|Crypt {|Agent B, Key (newK evs), 
    52                     Crypt {|Nonce NA, Key (newK evs)|} (shrK A),
    48                             Nonce NA, Nonce NB|} (shrK A),
    53                     Crypt {|Nonce NB, Key (newK evs)|} (shrK B)|}
    49                     Crypt {|Agent A, Key (newK evs)|} (shrK B)|}
    54                  # evs : yahalom"
    50                  # evs : yahalom"
    55 
    51 
    56          (*Bob receives the Server's (?) message and compares the Nonces with
    52          (*Alice receives the Server's (?) message, checks her Nonce, and
    57 	   those in the message he previously sent the Server.*)
    53            uses the new session key to send Bob his Nonce.*)
    58     YM4  "[| evs: yahalom;  A ~= B;  
    54     YM4  "[| evs: yahalom;  A ~= B;  
    59              Says S B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|}
    55              Says S A {|Crypt {|Agent B, Key K, Nonce NA, Nonce NB|} (shrK A),
       
    56                         X|}
    60                : set_of_list evs;
    57                : set_of_list evs;
    61              Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|}
    58              Says A B {|Agent A, Nonce NA|} : set_of_list evs |]
    62                : set_of_list evs |]
    59           ==> Says A B {|X, Crypt (Nonce NB) K|} # evs : yahalom"
    63           ==> (Says B A {|Nonce NA, X|}) # evs : yahalom"
       
    64 
       
    65          (*Alice checks her Nonce, then sends a dummy message to Bob,
       
    66            using the new session key.*)
       
    67     YM5  "[| evs: yahalom;  
       
    68              Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|}
       
    69                : set_of_list evs;
       
    70              Says A  B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |]
       
    71           ==> Says A B (Crypt (Agent A) K)  # evs : yahalom"
       
    72 
    60 
    73 end
    61 end