src/HOL/Auth/WooLam.thy
author paulson
Fri Jul 04 17:34:55 1997 +0200 (1997-07-04)
changeset 3500 0d8ad2f192d8
parent 3481 256f38c01b98
child 3519 ab0a9fbed4c0
permissions -rw-r--r--
New constant "certificate"--just an abbreviation
paulson@2274
     1
(*  Title:      HOL/Auth/WooLam
paulson@2274
     2
    ID:         $Id$
paulson@2274
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@2274
     4
    Copyright   1996  University of Cambridge
paulson@2274
     5
paulson@2274
     6
Inductive relation "woolam" for the Woo-Lam protocol.
paulson@2274
     7
paulson@2274
     8
Simplified version from page 11 of
paulson@2274
     9
  Abadi and Needham.  Prudent Engineering Practice for Cryptographic Protocols.
paulson@2274
    10
  IEEE Trans. S.E. 22(1), 1996, pages 6-15.
paulson@2274
    11
paulson@2274
    12
Note: this differs from the Woo-Lam protocol discussed by Lowe in his paper
paulson@2274
    13
  Some New Attacks upon Security Protocols.
paulson@2274
    14
  Computer Security Foundations Workshop, 1996.
paulson@2274
    15
*)
paulson@2274
    16
paulson@2274
    17
WooLam = Shared + 
paulson@2274
    18
paulson@2283
    19
consts  lost    :: agent set        (*No need for it to be a variable*)
paulson@2283
    20
	woolam  :: event list set
paulson@2283
    21
inductive woolam
paulson@2274
    22
  intrs 
paulson@2274
    23
         (*Initial trace is empty*)
paulson@2283
    24
    Nil  "[]: woolam"
paulson@2274
    25
paulson@2274
    26
         (*The spy MAY say anything he CAN say.  We do not expect him to
paulson@2274
    27
           invent new nonces here, but he can also use NS1.  Common to
paulson@2274
    28
           all similar protocols.*)
paulson@2283
    29
    Fake "[| evs: woolam;  B ~= Spy;  
paulson@2274
    30
             X: synth (analz (sees lost Spy evs)) |]
paulson@2283
    31
          ==> Says Spy B X  # evs : woolam"
paulson@2274
    32
paulson@2274
    33
         (*Alice initiates a protocol run*)
paulson@2283
    34
    WL1  "[| evs: woolam;  A ~= B |]
paulson@2283
    35
          ==> Says A B (Agent A) # evs : woolam"
paulson@2274
    36
paulson@2274
    37
         (*Bob responds to Alice's message with a challenge.*)
paulson@2516
    38
    WL2  "[| evs: woolam;  A ~= B;  
nipkow@3465
    39
             Says A' B (Agent A) : set evs |]
paulson@2516
    40
          ==> Says B A (Nonce NB) # evs : woolam"
paulson@2274
    41
paulson@2274
    42
         (*Alice responds to Bob's challenge by encrypting NB with her key.
paulson@2274
    43
           B is *not* properly determined -- Alice essentially broadcasts
paulson@2274
    44
           her reply.*)
paulson@3481
    45
    WL3  "[| evs: woolam;
nipkow@3465
    46
             Says A  B (Agent A)  : set evs;
nipkow@3465
    47
             Says B' A (Nonce NB) : set evs |]
paulson@2283
    48
          ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs : woolam"
paulson@2274
    49
paulson@3470
    50
         (*Bob forwards Alice's response to the Server.  NOTE: usually
paulson@3470
    51
           the messages are shown in chronological order, for clarity.
paulson@3470
    52
           But here, exchanging the two events would cause the lemma
paulson@3470
    53
           WL4_analz_sees_Spy to pick up the wrong assumption!*)
paulson@2283
    54
    WL4  "[| evs: woolam;  B ~= Server;  
nipkow@3465
    55
             Says A'  B X         : set evs;
nipkow@3465
    56
             Says A'' B (Agent A) : set evs |]
paulson@2283
    57
          ==> Says B Server {|Agent A, Agent B, X|} # evs : woolam"
paulson@2274
    58
paulson@2274
    59
         (*Server decrypts Alice's response for Bob.*)
paulson@2283
    60
    WL5  "[| evs: woolam;  B ~= Server;
paulson@2283
    61
             Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|}
nipkow@3465
    62
               : set evs |]
paulson@2283
    63
          ==> Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|})
paulson@2283
    64
                 # evs : woolam"
paulson@2274
    65
paulson@2274
    66
end