src/HOL/Auth/Yahalom.thy
author paulson
Fri Sep 13 13:16:57 1996 +0200 (1996-09-13)
changeset 1995 c80e58e78d9c
parent 1985 84cf16192e03
child 2032 1bbf1bdcaf56
permissions -rw-r--r--
Addition of Yahalom protocol
     1 (*  Title:      HOL/Auth/Yahalom
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     5 
     6 Inductive relation "yahalom" for the Yahalom protocol.
     7 
     8 From page 257 of
     9   Burrows, Abadi and Needham.  A Logic of Authentication.
    10   Proc. Royal Soc. 426 (1989)
    11 *)
    12 
    13 Yahalom = Shared + 
    14 
    15 consts  yahalom   :: "event list set"
    16 inductive yahalom
    17   intrs 
    18          (*Initial trace is empty*)
    19     Nil  "[]: yahalom"
    20 
    21          (*The enemy MAY say anything he CAN say.  We do not expect him to
    22            invent new nonces here, but he can also use NS1.  Common to
    23            all similar protocols.*)
    24     Fake "[| evs: yahalom;  B ~= Enemy;  X: synth (analz (sees Enemy evs)) |]
    25           ==> Says Enemy B X  # evs : yahalom"
    26 
    27          (*Alice initiates a protocol run*)
    28     YM1  "[| evs: yahalom;  A ~= B |]
    29           ==> Says A B {|Agent A, Nonce (newN evs)|} # evs : yahalom"
    30 
    31          (*Bob's response to Alice's message.  Bob doesn't know who 
    32 	   the sender is, hence the A' in the sender field.*)
    33     YM2  "[| evs: yahalom;  B ~= Server;
    34              Says A' B {|Agent A, Nonce NA|} : set_of_list evs |]
    35           ==> Says B Server 
    36                   {|Agent B, 
    37                     Crypt {|Agent A, Nonce NA, Nonce (newN evs)|} (shrK B)|}
    38                  # evs : yahalom"
    39 
    40          (*The Server receives Bob's message.  He responds by sending a
    41             new session key to Alice, with a packet for forwarding to Bob.*)
    42     YM3  "[| evs: yahalom;  A ~= Server;
    43              Says B' Server 
    44                   {|Agent B, Crypt {|Agent A, Nonce NA, Nonce NB|} (shrK B)|}
    45                : set_of_list evs |]
    46           ==> Says Server A
    47                   {|Crypt {|Agent B, Key (newK evs), 
    48                             Nonce NA, Nonce NB|} (shrK A),
    49                     Crypt {|Agent A, Key (newK evs)|} (shrK B)|}
    50                  # evs : yahalom"
    51 
    52          (*Alice receives the Server's (?) message, checks her Nonce, and
    53            uses the new session key to send Bob his Nonce.*)
    54     YM4  "[| evs: yahalom;  A ~= B;  
    55              Says S A {|Crypt {|Agent B, Key K, Nonce NA, Nonce NB|} (shrK A),
    56                         X|}
    57                : set_of_list evs;
    58              Says A B {|Agent A, Nonce NA|} : set_of_list evs |]
    59           ==> Says A B {|X, Crypt (Nonce NB) K|} # evs : yahalom"
    60 
    61 end