src/HOL/Auth/WooLam.thy
author paulson
Tue Nov 11 11:16:18 1997 +0100 (1997-11-11)
changeset 4198 c63639beeff1
parent 3683 aafe719dff14
child 5434 9b4bed3f394c
permissions -rw-r--r--
Fixed spelling error
     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  :: event list set
    20 inductive woolam
    21   intrs 
    22          (*Initial trace is empty*)
    23     Nil  "[]: woolam"
    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;  B ~= Spy;  
    29              X: synth (analz (spies evs)) |]
    30           ==> Says Spy B X  # evs : woolam"
    31 
    32          (*Alice initiates a protocol run*)
    33     WL1  "[| evs1: woolam;  A ~= B |]
    34           ==> Says A B (Agent A) # evs1 : woolam"
    35 
    36          (*Bob responds to Alice's message with a challenge.*)
    37     WL2  "[| evs2: woolam;  A ~= B;  
    38              Says A' B (Agent A) : set evs2 |]
    39           ==> Says B A (Nonce NB) # evs2 : woolam"
    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  "[| evs3: woolam;
    45              Says A  B (Agent A)  : set evs3;
    46              Says B' A (Nonce NB) : set evs3 |]
    47           ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs3 : woolam"
    48 
    49          (*Bob forwards Alice's response to the Server.  NOTE: usually
    50            the messages are shown in chronological order, for clarity.
    51            But here, exchanging the two events would cause the lemma
    52            WL4_analz_spies to pick up the wrong assumption!*)
    53     WL4  "[| evs4: woolam;  B ~= Server;  
    54              Says A'  B X         : set evs4;
    55              Says A'' B (Agent A) : set evs4 |]
    56           ==> Says B Server {|Agent A, Agent B, X|} # evs4 : woolam"
    57 
    58          (*Server decrypts Alice's response for Bob.*)
    59     WL5  "[| evs5: woolam;  B ~= Server;
    60              Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|}
    61                : set evs5 |]
    62           ==> Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|})
    63                  # evs5 : woolam"
    64 
    65 end