src/HOL/Auth/Public.thy
author paulson
Tue Nov 11 11:16:18 1997 +0100 (1997-11-11)
changeset 4198 c63639beeff1
parent 3683 aafe719dff14
child 5183 89f162de39cf
permissions -rw-r--r--
Fixed spelling error
     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 Public = Event + 
    12 
    13 consts
    14   pubK    :: agent => key
    15 
    16 syntax
    17   priK    :: agent => key
    18 
    19 translations  (*BEWARE! expressions like  (inj priK)  will NOT work!*)
    20   "priK x"  == "invKey(pubK x)"
    21 
    22 primrec initState agent
    23         (*Agents know their private key and all public keys*)
    24   initState_Server  "initState Server     =    
    25  		         insert (Key (priK Server)) (Key `` range pubK)"
    26   initState_Friend  "initState (Friend i) =    
    27  		         insert (Key (priK (Friend i))) (Key `` range pubK)"
    28   initState_Spy     "initState Spy        =    
    29  		         (Key``invKey``pubK``bad) Un (Key `` range pubK)"
    30 
    31 
    32 rules
    33   (*Public keys are disjoint, and never clash with private keys*)
    34   inj_pubK        "inj pubK"
    35   priK_neq_pubK   "priK A ~= pubK B"
    36 
    37 end