src/HOL/Auth/Shared.thy
author paulson
Sat Aug 17 14:55:08 2002 +0200 (2002-08-17)
changeset 13507 febb8e5d2a9d
parent 12415 74977582a585
child 13907 2bc462b99e70
permissions -rw-r--r--
tidying of Isar scripts
paulson@1934
     1
(*  Title:      HOL/Auth/Shared
paulson@1934
     2
    ID:         $Id$
paulson@1934
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@1934
     4
    Copyright   1996  University of Cambridge
paulson@1934
     5
paulson@1934
     6
Theory of Shared Keys (common to all symmetric-key protocols)
paulson@1934
     7
paulson@3512
     8
Shared, long-term keys; initial states of agents
paulson@1934
     9
*)
paulson@1934
    10
paulson@11104
    11
theory Shared = Event
paulson@11104
    12
files ("Shared_lemmas.ML"):
paulson@1934
    13
paulson@1934
    14
consts
paulson@11104
    15
  shrK    :: "agent => key"  (*symmetric keys*)
paulson@1967
    16
paulson@11104
    17
axioms
paulson@11270
    18
  isSym_keys: "K \<in> symKeys"	(*All keys are symmetric*)
paulson@11104
    19
  inj_shrK:   "inj shrK"	(*No two agents have the same long-term key*)
paulson@1934
    20
berghofe@5183
    21
primrec
paulson@2319
    22
        (*Server knows all long-term keys; other agents know only their own*)
paulson@11104
    23
  initState_Server:  "initState Server     = Key ` range shrK"
paulson@11104
    24
  initState_Friend:  "initState (Friend i) = {Key (shrK (Friend i))}"
paulson@11104
    25
  initState_Spy:     "initState Spy        = Key`shrK`bad"
paulson@2032
    26
paulson@1934
    27
paulson@11104
    28
axioms
paulson@2516
    29
  (*Unlike the corresponding property of nonces, this cannot be proved.
paulson@2516
    30
    We have infinitely many agents and there is nothing to stop their
paulson@2516
    31
    long-term keys from exhausting all the natural numbers.  The axiom
paulson@2516
    32
    assumes that their keys are dispersed so as to leave room for infinitely
paulson@2516
    33
    many fresh session keys.  We could, alternatively, restrict agents to
paulson@2516
    34
    an unspecified finite number.*)
paulson@11104
    35
  Key_supply_ax:  "finite KK ==> EX K. K ~: KK & Key K ~: used evs"
paulson@11104
    36
paulson@11104
    37
use "Shared_lemmas.ML"
paulson@11104
    38
paulson@11104
    39
(*Lets blast_tac perform this step without needing the simplifier*)
paulson@11104
    40
lemma invKey_shrK_iff [iff]:
paulson@11270
    41
     "(Key (invKey K) \<in> X) = (Key K \<in> X)"
paulson@13507
    42
by auto
paulson@11104
    43
paulson@11104
    44
(*Specialized methods*)
paulson@11104
    45
paulson@11104
    46
method_setup analz_freshK = {*
paulson@11104
    47
    Method.no_args
paulson@11104
    48
     (Method.METHOD
paulson@11104
    49
      (fn facts => EVERY [REPEAT_FIRST (resolve_tac [allI, impI]),
paulson@11104
    50
                          REPEAT_FIRST (rtac analz_image_freshK_lemma),
paulson@11104
    51
                          ALLGOALS (asm_simp_tac analz_image_freshK_ss)])) *}
paulson@11104
    52
    "for proving the Session Key Compromise theorem"
paulson@11104
    53
paulson@11104
    54
method_setup possibility = {*
paulson@11270
    55
    Method.ctxt_args (fn ctxt =>
paulson@11270
    56
        Method.METHOD (fn facts =>
paulson@11270
    57
            gen_possibility_tac (Simplifier.get_local_simpset ctxt))) *}
paulson@11104
    58
    "for proving possibility theorems"
paulson@2516
    59
paulson@12415
    60
lemma knows_subset_knows_Cons: "knows A evs <= knows A (e # evs)"
paulson@12415
    61
by (induct e, auto simp: knows_Cons)
paulson@12415
    62
paulson@1934
    63
end