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