src/HOL/Auth/Shared.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 5183 89f162de39cf
child 10833 c0844a30ea4e
permissions -rw-r--r--
hide many names from Datatype_Universe.
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/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
Theory of Shared Keys (common to all symmetric-key protocols)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     7
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3472
diff changeset
     8
Shared, long-term keys; initial states of agents
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     9
*)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    10
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3472
diff changeset
    11
Shared = Event + Finite +
1934
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
consts
1943
20574dca5a3e Renaming and simplification
paulson
parents: 1934
diff changeset
    14
  shrK    :: agent => key  (*symmetric keys*)
1967
0ff58b41c037 "bad" set simplifies statements of many theorems
paulson
parents: 1965
diff changeset
    15
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    16
rules
3472
fb3c38c88c08 Deleted the obsolete operators newK, newN and nPair
paulson
parents: 3414
diff changeset
    17
  isSym_keys "isSymKey K"	(*All keys are symmetric*)
fb3c38c88c08 Deleted the obsolete operators newK, newN and nPair
paulson
parents: 3414
diff changeset
    18
  inj_shrK   "inj shrK"		(*No two agents have the same long-term key*)
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    19
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 3683
diff changeset
    20
primrec
2319
95f0d5243c85 Updating of comments
paulson
parents: 2264
diff changeset
    21
        (*Server knows all long-term keys; other agents know only their own*)
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3512
diff changeset
    22
  initState_Server  "initState Server     = Key `` range shrK"
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3512
diff changeset
    23
  initState_Friend  "initState (Friend i) = {Key (shrK (Friend i))}"
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3519
diff changeset
    24
  initState_Spy     "initState Spy        = Key``shrK``bad"
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2012
diff changeset
    25
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    26
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    27
rules
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    28
  (*Unlike the corresponding property of nonces, this cannot be proved.
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    29
    We have infinitely many agents and there is nothing to stop their
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    30
    long-term keys from exhausting all the natural numbers.  The axiom
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    31
    assumes that their keys are dispersed so as to leave room for infinitely
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    32
    many fresh session keys.  We could, alternatively, restrict agents to
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    33
    an unspecified finite number.*)
3414
804c8a178a7f Modified a few defs and proofs because of the changes to theory Finite.thy.
nipkow
parents: 2516
diff changeset
    34
  Key_supply_ax  "finite KK ==> EX K. K ~: KK & Key K ~: used evs"
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    35
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    36
end