src/HOL/Auth/WooLam.thy
author paulson
Thu Nov 28 15:56:04 1996 +0100 (1996-11-28)
changeset 2274 1b1b46adc9b3
child 2283 68829cf138fc
permissions -rw-r--r--
Addition of Woo-Lam protocol
     1 (*  Title:      HOL/Auth/WooLam
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     5 
     6 Inductive relation "woolam" for the Woo-Lam protocol.
     7 
     8 Simplified version from page 11 of
     9   Abadi and Needham.  Prudent Engineering Practice for Cryptographic Protocols.
    10   IEEE Trans. S.E. 22(1), 1996, pages 6-15.
    11 
    12 Note: this differs from the Woo-Lam protocol discussed by Lowe in his paper
    13   Some New Attacks upon Security Protocols.
    14   Computer Security Foundations Workshop, 1996.
    15 *)
    16 
    17 WooLam = Shared + 
    18 
    19 consts  woolam   :: "agent set => event list set"
    20 inductive "woolam lost"
    21   intrs 
    22          (*Initial trace is empty*)
    23     Nil  "[]: woolam lost"
    24 
    25          (*The spy MAY say anything he CAN say.  We do not expect him to
    26            invent new nonces here, but he can also use NS1.  Common to
    27            all similar protocols.*)
    28     Fake "[| evs: woolam lost;  B ~= Spy;  
    29              X: synth (analz (sees lost Spy evs)) |]
    30           ==> Says Spy B X  # evs : woolam lost"
    31 
    32          (*Alice initiates a protocol run*)
    33     WL1  "[| evs: woolam lost;  A ~= B |]
    34           ==> Says A B (Agent A) # evs : woolam lost"
    35 
    36          (*Bob responds to Alice's message with a challenge.*)
    37     WL2  "[| evs: woolam lost;  A ~= B;
    38              Says A' B (Agent A) : set_of_list evs |]
    39           ==> Says B A (Nonce (newN evs)) # evs : woolam lost"
    40 
    41          (*Alice responds to Bob's challenge by encrypting NB with her key.
    42            B is *not* properly determined -- Alice essentially broadcasts
    43            her reply.*)
    44     WL3  "[| evs: woolam lost;  A ~= B;
    45              Says B' A (Nonce NB) : set_of_list evs;
    46              Says A  B (Agent A)  : set_of_list evs |]
    47           ==> Says A B (Crypt (Nonce NB) (shrK A)) # evs : woolam lost"
    48 
    49          (*Bob forwards Alice's response to the Server.*)
    50     WL4  "[| evs: woolam lost;  B ~= Server;  
    51              Says A'  B X         : set_of_list evs;
    52              Says A'' B (Agent A) : set_of_list evs |]
    53           ==> Says B Server {|Agent A, Agent B, X|} # evs : woolam lost"
    54 
    55          (*Server decrypts Alice's response for Bob.*)
    56     WL5  "[| evs: woolam lost;  B ~= Server;
    57              Says B' Server {|Agent A, Agent B, Crypt (Nonce NB) (shrK A)|}
    58                : set_of_list evs |]
    59           ==> Says Server B (Crypt {|Agent A, Nonce NB|} (shrK B))
    60                  # evs : woolam lost"
    61 
    62 end