1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/TutorialI/Protocol/Public.thy	Wed Apr 11 11:53:54 2001 +0200
     1.3 @@ -0,0 +1,46 @@
     1.4 +(*  Title:      HOL/Auth/Public
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1996  University of Cambridge
     1.8 +
     1.9 +Theory of Public Keys (common to all public-key protocols)
    1.10 +
    1.11 +Private and public keys; initial states of agents
    1.12 +*)
    1.13 +
    1.14 +theory Public = Event
    1.15 +files ("Public_lemmas.ML"):
    1.16 +
    1.17 +consts
    1.18 +  pubK    :: "agent => key"
    1.19 +
    1.20 +syntax
    1.21 +  priK    :: "agent => key"
    1.22 +
    1.23 +translations  (*BEWARE! expressions like  (inj priK)  will NOT work!*)
    1.24 +  "priK x"  == "invKey(pubK x)"
    1.25 +
    1.26 +primrec
    1.27 +        (*Agents know their private key and all public keys*)
    1.28 +  initState_Server:  "initState Server     =    
    1.29 + 		         insert (Key (priK Server)) (Key ` range pubK)"
    1.30 +  initState_Friend:  "initState (Friend i) =    
    1.31 + 		         insert (Key (priK (Friend i))) (Key ` range pubK)"
    1.32 +  initState_Spy:     "initState Spy        =    
    1.33 + 		         (Key`invKey`pubK`bad) Un (Key ` range pubK)"
    1.34 +
    1.35 +
    1.36 +axioms
    1.37 +  (*Public keys are disjoint, and never clash with private keys*)
    1.38 +  inj_pubK:        "inj pubK"
    1.39 +  priK_neq_pubK:   "priK A ~= pubK B"
    1.40 +
    1.41 +use "Public_lemmas.ML"
    1.42 +
    1.43 +(*Specialized methods*)
    1.44 +
    1.45 +method_setup possibility = {*
    1.46 +    Method.no_args (Method.METHOD (fn facts => possibility_tac)) *}
    1.47 +    "for proving possibility theorems"
    1.48 +
    1.49 +end