src/HOL/Auth/WooLam.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 5434 9b4bed3f394c
child 11185 1b737b4c2108
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Auth/WooLam
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
     2
    ID:         $Id$
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
     4
    Copyright   1996  University of Cambridge
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
     5
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
     6
Inductive relation "woolam" for the Woo-Lam protocol.
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
     7
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
     8
Simplified version from page 11 of
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
     9
  Abadi and Needham.  Prudent Engineering Practice for Cryptographic Protocols.
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    10
  IEEE Trans. S.E. 22(1), 1996, pages 6-15.
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    11
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    12
Note: this differs from the Woo-Lam protocol discussed by Lowe in his paper
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    13
  Some New Attacks upon Security Protocols.
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    14
  Computer Security Foundations Workshop, 1996.
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    15
*)
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    16
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    17
WooLam = Shared + 
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    18
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3481
diff changeset
    19
consts  woolam  :: event list set
2283
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
    20
inductive woolam
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    21
  intrs 
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    22
         (*Initial trace is empty*)
2283
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
    23
    Nil  "[]: woolam"
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    24
5434
9b4bed3f394c Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents: 3683
diff changeset
    25
         (** These rules allow agents to send messages to themselves **)
9b4bed3f394c Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents: 3683
diff changeset
    26
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    27
         (*The spy MAY say anything he CAN say.  We do not expect him to
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    28
           invent new nonces here, but he can also use NS1.  Common to
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    29
           all similar protocols.*)
5434
9b4bed3f394c Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents: 3683
diff changeset
    30
    Fake "[| evs: woolam;  X: synth (analz (spies evs)) |]
2283
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
    31
          ==> Says Spy B X  # evs : woolam"
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    32
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    33
         (*Alice initiates a protocol run*)
5434
9b4bed3f394c Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents: 3683
diff changeset
    34
    WL1  "[| evs1: woolam |]
3659
eddedfe2f3f8 Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents: 3519
diff changeset
    35
          ==> Says A B (Agent A) # evs1 : woolam"
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    36
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    37
         (*Bob responds to Alice's message with a challenge.*)
5434
9b4bed3f394c Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents: 3683
diff changeset
    38
    WL2  "[| evs2: woolam;  Says A' B (Agent A) : set evs2 |]
3659
eddedfe2f3f8 Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents: 3519
diff changeset
    39
          ==> Says B A (Nonce NB) # evs2 : woolam"
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    40
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    41
         (*Alice responds to Bob's challenge by encrypting NB with her key.
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    42
           B is *not* properly determined -- Alice essentially broadcasts
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    43
           her reply.*)
3659
eddedfe2f3f8 Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents: 3519
diff changeset
    44
    WL3  "[| evs3: woolam;
eddedfe2f3f8 Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents: 3519
diff changeset
    45
             Says A  B (Agent A)  : set evs3;
eddedfe2f3f8 Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents: 3519
diff changeset
    46
             Says B' A (Nonce NB) : set evs3 |]
eddedfe2f3f8 Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents: 3519
diff changeset
    47
          ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs3 : woolam"
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    48
3470
8160cc3f6d40 Added a comment
paulson
parents: 3465
diff changeset
    49
         (*Bob forwards Alice's response to the Server.  NOTE: usually
8160cc3f6d40 Added a comment
paulson
parents: 3465
diff changeset
    50
           the messages are shown in chronological order, for clarity.
8160cc3f6d40 Added a comment
paulson
parents: 3465
diff changeset
    51
           But here, exchanging the two events would cause the lemma
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3659
diff changeset
    52
           WL4_analz_spies to pick up the wrong assumption!*)
5434
9b4bed3f394c Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents: 3683
diff changeset
    53
    WL4  "[| evs4: woolam;  
3659
eddedfe2f3f8 Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents: 3519
diff changeset
    54
             Says A'  B X         : set evs4;
eddedfe2f3f8 Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents: 3519
diff changeset
    55
             Says A'' B (Agent A) : set evs4 |]
eddedfe2f3f8 Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents: 3519
diff changeset
    56
          ==> Says B Server {|Agent A, Agent B, X|} # evs4 : woolam"
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    57
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    58
         (*Server decrypts Alice's response for Bob.*)
5434
9b4bed3f394c Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents: 3683
diff changeset
    59
    WL5  "[| evs5: woolam;  
2283
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
    60
             Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|}
3659
eddedfe2f3f8 Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents: 3519
diff changeset
    61
               : set evs5 |]
2283
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
    62
          ==> Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|})
3659
eddedfe2f3f8 Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents: 3519
diff changeset
    63
                 # evs5 : woolam"
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    64
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    65
end