src/HOL/Auth/NS_Shared.thy
author paulson
Fri, 11 Jul 1997 13:26:15 +0200
changeset 3512 9dcb4daa15e8
parent 3465 e85c24717cad
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:
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Auth/NS_Shared
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     2
    ID:         $Id$
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     4
    Copyright   1996  University of Cambridge
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     5
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     6
Inductive relation "ns_shared" for Needham-Schroeder Shared-Key protocol.
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     7
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     8
From page 247 of
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     9
  Burrows, Abadi and Needham.  A Logic of Authentication.
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    10
  Proc. Royal Soc. 426 (1989)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    11
*)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    12
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    13
NS_Shared = Shared + 
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    14
2378
fc103154ad8f Removed needless quotation marks
paulson
parents: 2284
diff changeset
    15
consts  ns_shared   :: agent set => event list set
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 1997
diff changeset
    16
inductive "ns_shared lost"
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    17
  intrs 
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    18
         (*Initial trace is empty*)
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 1997
diff changeset
    19
    Nil  "[]: ns_shared lost"
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    20
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 1997
diff changeset
    21
         (*The spy MAY say anything he CAN say.  We do not expect him to
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    22
           invent new nonces here, but he can also use NS1.  Common to
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    23
           all similar protocols.*)
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 1997
diff changeset
    24
    Fake "[| evs: ns_shared lost;  B ~= Spy;  
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 1997
diff changeset
    25
             X: synth (analz (sees lost Spy evs)) |]
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 1997
diff changeset
    26
          ==> Says Spy B X # evs : ns_shared lost"
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    27
1965
789c12ea0b30 Stronger proofs; work for Otway-Rees
paulson
parents: 1943
diff changeset
    28
         (*Alice initiates a protocol run, requesting to talk to any B*)
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    29
    NS1  "[| evs: ns_shared lost;  A ~= Server;  Nonce NA ~: used evs |]
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    30
          ==> Says A Server {|Agent A, Agent B, Nonce NA|} # evs
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    31
                :  ns_shared lost"
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    32
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    33
         (*Server's response to Alice's message.
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    34
           !! It may respond more than once to A's request !!
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    35
	   Server doesn't know who the true sender is, hence the A' in
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    36
               the sender field.*)
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    37
    NS2  "[| evs: ns_shared lost;  A ~= B;  A ~= Server;  Key KAB ~: used evs;
3465
e85c24717cad set_of_list -> set
nipkow
parents: 2516
diff changeset
    38
             Says A' Server {|Agent A, Agent B, Nonce NA|} : set evs |]
2451
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2378
diff changeset
    39
          ==> Says Server A 
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2378
diff changeset
    40
                (Crypt (shrK A)
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    41
                   {|Nonce NA, Agent B, Key KAB,
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    42
                     (Crypt (shrK B) {|Key KAB, Agent A|})|}) 
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2131
diff changeset
    43
                # evs : ns_shared lost"
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    44
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    45
          (*We can't assume S=Server.  Agent A "remembers" her nonce.
1997
6efba890341e No longer assumes Alice is not the Enemy in NS3.
paulson
parents: 1976
diff changeset
    46
            Can inductively show A ~= Server*)
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 1997
diff changeset
    47
    NS3  "[| evs: ns_shared lost;  A ~= B;
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2131
diff changeset
    48
             Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|}) 
3465
e85c24717cad set_of_list -> set
nipkow
parents: 2516
diff changeset
    49
               : set evs;
e85c24717cad set_of_list -> set
nipkow
parents: 2516
diff changeset
    50
             Says A Server {|Agent A, Agent B, Nonce NA|} : set evs |]
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 1997
diff changeset
    51
          ==> Says A B X # evs : ns_shared lost"
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    52
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    53
         (*Bob's nonce exchange.  He does not know who the message came
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    54
           from, but responds to A because she is mentioned inside.*)
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    55
    NS4  "[| evs: ns_shared lost;  A ~= B;  Nonce NB ~: used evs;
3465
e85c24717cad set_of_list -> set
nipkow
parents: 2516
diff changeset
    56
             Says A' B (Crypt (shrK B) {|Key K, Agent A|}) : set evs |]
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    57
          ==> Says B A (Crypt K (Nonce NB)) # evs
2451
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2378
diff changeset
    58
                : ns_shared lost"
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    59
2069
a1c623f70407 Addition of Revl rule, and tidying
paulson
parents: 2032
diff changeset
    60
         (*Alice responds with Nonce NB if she has seen the key before.
a1c623f70407 Addition of Revl rule, and tidying
paulson
parents: 2032
diff changeset
    61
           Maybe should somehow check Nonce NA again.
a1c623f70407 Addition of Revl rule, and tidying
paulson
parents: 2032
diff changeset
    62
           We do NOT send NB-1 or similar as the Spy cannot spoof such things.
a1c623f70407 Addition of Revl rule, and tidying
paulson
parents: 2032
diff changeset
    63
           Letting the Spy add or subtract 1 lets him send ALL nonces.
a1c623f70407 Addition of Revl rule, and tidying
paulson
parents: 2032
diff changeset
    64
           Instead we distinguish the messages by sending the nonce twice.*)
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 1997
diff changeset
    65
    NS5  "[| evs: ns_shared lost;  A ~= B;  
3465
e85c24717cad set_of_list -> set
nipkow
parents: 2516
diff changeset
    66
             Says B' A (Crypt K (Nonce NB)) : set evs;
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2131
diff changeset
    67
             Says S  A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
3465
e85c24717cad set_of_list -> set
nipkow
parents: 2516
diff changeset
    68
               : set evs |]
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2131
diff changeset
    69
          ==> Says A B (Crypt K {|Nonce NB, Nonce NB|}) # evs : ns_shared lost"
2069
a1c623f70407 Addition of Revl rule, and tidying
paulson
parents: 2032
diff changeset
    70
  
a1c623f70407 Addition of Revl rule, and tidying
paulson
parents: 2032
diff changeset
    71
         (*This message models possible leaks of session keys.
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2069
diff changeset
    72
           The two Nonces identify the protocol run: the rule insists upon
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2069
diff changeset
    73
           the true senders in order to make them accurate.*)
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2069
diff changeset
    74
    Oops "[| evs: ns_shared lost;  A ~= Spy;
3465
e85c24717cad set_of_list -> set
nipkow
parents: 2516
diff changeset
    75
             Says B A (Crypt K (Nonce NB)) : set evs;
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2131
diff changeset
    76
             Says Server A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
3465
e85c24717cad set_of_list -> set
nipkow
parents: 2516
diff changeset
    77
               : set evs |]
2069
a1c623f70407 Addition of Revl rule, and tidying
paulson
parents: 2032
diff changeset
    78
          ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : ns_shared lost"
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    79
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    80
end