src/HOL/Auth/WooLam.thy
author paulson
Thu Dec 19 11:58:39 1996 +0100 (1996-12-19)
changeset 2451 ce85a2aafc7a
parent 2283 68829cf138fc
child 2516 4d68fbe6378b
permissions -rw-r--r--
Extensive tidying and simplification, largely stemming from
changing newN and newK to take an integer argument
     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  lost    :: agent set        (*No need for it to be a variable*)
    20 	woolam  :: event list set
    21 inductive woolam
    22   intrs 
    23          (*Initial trace is empty*)
    24     Nil  "[]: woolam"
    25 
    26          (*The spy MAY say anything he CAN say.  We do not expect him to
    27            invent new nonces here, but he can also use NS1.  Common to
    28            all similar protocols.*)
    29     Fake "[| evs: woolam;  B ~= Spy;  
    30              X: synth (analz (sees lost Spy evs)) |]
    31           ==> Says Spy B X  # evs : woolam"
    32 
    33          (*Alice initiates a protocol run*)
    34     WL1  "[| evs: woolam;  A ~= B |]
    35           ==> Says A B (Agent A) # evs : woolam"
    36 
    37          (*Bob responds to Alice's message with a challenge.*)
    38     WL2  "[| evs: woolam;  A ~= B;
    39              Says A' B (Agent A) : set_of_list evs |]
    40           ==> Says B A (Nonce (newN(length evs))) # evs : woolam"
    41 
    42          (*Alice responds to Bob's challenge by encrypting NB with her key.
    43            B is *not* properly determined -- Alice essentially broadcasts
    44            her reply.*)
    45     WL3  "[| evs: woolam;  A ~= B;
    46              Says B' A (Nonce NB) : set_of_list evs;
    47              Says A  B (Agent A)  : set_of_list evs |]
    48           ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs : woolam"
    49 
    50          (*Bob forwards Alice's response to the Server.*)
    51     WL4  "[| evs: woolam;  B ~= Server;  
    52              Says A'  B X         : set_of_list evs;
    53              Says A'' B (Agent A) : set_of_list evs |]
    54           ==> Says B Server {|Agent A, Agent B, X|} # evs : woolam"
    55 
    56          (*Server decrypts Alice's response for Bob.*)
    57     WL5  "[| evs: woolam;  B ~= Server;
    58              Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|}
    59                : set_of_list evs |]
    60           ==> Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|})
    61                  # evs : woolam"
    62 
    63 end