src/HOL/Auth/Public.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 5183 89f162de39cf
child 10833 c0844a30ea4e
permissions -rw-r--r--
hide many names from Datatype_Universe.

(*  Title:      HOL/Auth/Public
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1996  University of Cambridge

Theory of Public Keys (common to all public-key protocols)

Private and public keys; initial states of agents
*)

Public = Event + 

consts
  pubK    :: agent => key

syntax
  priK    :: agent => key

translations  (*BEWARE! expressions like  (inj priK)  will NOT work!*)
  "priK x"  == "invKey(pubK x)"

primrec
        (*Agents know their private key and all public keys*)
  initState_Server  "initState Server     =    
 		         insert (Key (priK Server)) (Key `` range pubK)"
  initState_Friend  "initState (Friend i) =    
 		         insert (Key (priK (Friend i))) (Key `` range pubK)"
  initState_Spy     "initState Spy        =    
 		         (Key``invKey``pubK``bad) Un (Key `` range pubK)"


rules
  (*Public keys are disjoint, and never clash with private keys*)
  inj_pubK        "inj pubK"
  priK_neq_pubK   "priK A ~= pubK B"

end