src/HOL/Auth/Shared.thy
author paulson
Fri, 11 Jul 1997 13:26:15 +0200
changeset 3512 9dcb4daa15e8
parent 3472 fb3c38c88c08
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/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
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    20
primrec initState agent
2319
95f0d5243c85 Updating of comments
paulson
parents: 2264
diff changeset
    21
        (*Server knows all long-term keys; other agents know only their own*)
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2012
diff changeset
    22
  initState_Server  "initState lost Server     = Key `` range shrK"
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2012
diff changeset
    23
  initState_Friend  "initState lost (Friend i) = {Key (shrK (Friend i))}"
2064
5a5e508e2a2b Simple tidying
paulson
parents: 2032
diff changeset
    24
  initState_Spy     "initState lost Spy        = Key``shrK``lost"
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