src/HOL/Auth/WooLam.thy
author paulson
Fri, 11 Jul 1997 13:26:15 +0200
changeset 3512 9dcb4daa15e8
parent 3481 256f38c01b98
child 3519 ab0a9fbed4c0
permissions -rw-r--r--
Moving common declarations and proofs from theories "Shared" and "Public" to "Event". NB the original "Event" theory was later renamed "Shared". Addition of the Notes constructor to datatype "event".
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
2283
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
    19
consts  lost    :: agent set        (*No need for it to be a variable*)
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
    20
	woolam  :: event list set
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
    21
inductive woolam
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    22
  intrs 
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    23
         (*Initial trace is empty*)
2283
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
    24
    Nil  "[]: woolam"
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    25
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    26
         (*The spy MAY say anything he CAN say.  We do not expect him to
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    27
           invent new nonces here, but he can also use NS1.  Common to
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    28
           all similar protocols.*)
2283
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
    29
    Fake "[| evs: woolam;  B ~= Spy;  
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    30
             X: synth (analz (sees lost Spy 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*)
2283
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
    34
    WL1  "[| evs: woolam;  A ~= B |]
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
    35
          ==> Says A B (Agent A) # evs : 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.*)
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    38
    WL2  "[| evs: woolam;  A ~= B;  
3465
e85c24717cad set_of_list -> set
nipkow
parents: 2516
diff changeset
    39
             Says A' B (Agent A) : set evs |]
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    40
          ==> Says B A (Nonce NB) # evs : woolam"
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    41
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    42
         (*Alice responds to Bob's challenge by encrypting NB with her key.
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    43
           B is *not* properly determined -- Alice essentially broadcasts
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    44
           her reply.*)
3481
256f38c01b98 Deleted a redundant A~=B in rules that refer to a previous event
paulson
parents: 3470
diff changeset
    45
    WL3  "[| evs: woolam;
3465
e85c24717cad set_of_list -> set
nipkow
parents: 2516
diff changeset
    46
             Says A  B (Agent A)  : set evs;
e85c24717cad set_of_list -> set
nipkow
parents: 2516
diff changeset
    47
             Says B' A (Nonce NB) : set evs |]
2283
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
    48
          ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs : woolam"
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    49
3470
8160cc3f6d40 Added a comment
paulson
parents: 3465
diff changeset
    50
         (*Bob forwards Alice's response to the Server.  NOTE: usually
8160cc3f6d40 Added a comment
paulson
parents: 3465
diff changeset
    51
           the messages are shown in chronological order, for clarity.
8160cc3f6d40 Added a comment
paulson
parents: 3465
diff changeset
    52
           But here, exchanging the two events would cause the lemma
8160cc3f6d40 Added a comment
paulson
parents: 3465
diff changeset
    53
           WL4_analz_sees_Spy to pick up the wrong assumption!*)
2283
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
    54
    WL4  "[| evs: woolam;  B ~= Server;  
3465
e85c24717cad set_of_list -> set
nipkow
parents: 2516
diff changeset
    55
             Says A'  B X         : set evs;
e85c24717cad set_of_list -> set
nipkow
parents: 2516
diff changeset
    56
             Says A'' B (Agent A) : set evs |]
2283
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
    57
          ==> Says B Server {|Agent A, Agent B, X|} # evs : woolam"
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    58
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    59
         (*Server decrypts Alice's response for Bob.*)
2283
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
    60
    WL5  "[| evs: woolam;  B ~= Server;
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
    61
             Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|}
3465
e85c24717cad set_of_list -> set
nipkow
parents: 2516
diff changeset
    62
               : set evs |]
2283
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
    63
          ==> Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|})
68829cf138fc Swapping arguments of Crypt; removing argument lost
paulson
parents: 2274
diff changeset
    64
                 # evs : woolam"
2274
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    65
1b1b46adc9b3 Addition of Woo-Lam protocol
paulson
parents:
diff changeset
    66
end