doc-src/TutorialI/Protocol/Public.thy
author haftmann
Fri Jun 17 16:12:49 2005 +0200 (2005-06-17)
changeset 16417 9bc16273c2d4
parent 11250 c8bbf4c4bc2d
child 23925 ee98c2528a8f
permissions -rw-r--r--
migrated theory headers to new format
     1 (*  Title:      HOL/Auth/Public
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     5 
     6 Theory of Public Keys (common to all public-key protocols)
     7 
     8 Private and public keys; initial states of agents
     9 *)
    10 
    11 theory Public imports Event
    12 uses ("Public_lemmas.ML") begin
    13 
    14 consts
    15   pubK    :: "agent => key"
    16 
    17 syntax
    18   priK    :: "agent => key"
    19 
    20 translations  (*BEWARE! expressions like  (inj priK)  will NOT work!*)
    21   "priK x"  == "invKey(pubK x)"
    22 
    23 primrec
    24         (*Agents know their private key and all public keys*)
    25   initState_Server:  "initState Server     =    
    26  		         insert (Key (priK Server)) (Key ` range pubK)"
    27   initState_Friend:  "initState (Friend i) =    
    28  		         insert (Key (priK (Friend i))) (Key ` range pubK)"
    29   initState_Spy:     "initState Spy        =    
    30  		         (Key`invKey`pubK`bad) Un (Key ` range pubK)"
    31 
    32 
    33 axioms
    34   (*Public keys are disjoint, and never clash with private keys*)
    35   inj_pubK:        "inj pubK"
    36   priK_neq_pubK:   "priK A ~= pubK B"
    37 
    38 use "Public_lemmas.ML"
    39 
    40 (*Specialized methods*)
    41 
    42 method_setup possibility = {*
    43     Method.no_args (Method.METHOD (fn facts => possibility_tac)) *}
    44     "for proving possibility theorems"
    45 
    46 end