src/HOL/Auth/Public.thy
author paulson
Fri Sep 19 18:27:31 1997 +0200 (1997-09-19)
changeset 3686 4b484805b4c4
parent 3683 aafe719dff14
child 5183 89f162de39cf
permissions -rw-r--r--
First working version with Oops event for session keys
paulson@2318
     1
(*  Title:      HOL/Auth/Public
paulson@2318
     2
    ID:         $Id$
paulson@2318
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@2318
     4
    Copyright   1996  University of Cambridge
paulson@2318
     5
paulson@3512
     6
Theory of Public Keys (common to all public-key protocols)
paulson@2318
     7
paulson@3512
     8
Private and public keys; initial states of agents
paulson@2318
     9
*)
paulson@2318
    10
paulson@3512
    11
Public = Event + 
paulson@2318
    12
paulson@2318
    13
consts
paulson@2318
    14
  pubK    :: agent => key
paulson@2318
    15
paulson@2318
    16
syntax
paulson@2318
    17
  priK    :: agent => key
paulson@2318
    18
paulson@3478
    19
translations  (*BEWARE! expressions like  (inj priK)  will NOT work!*)
paulson@2318
    20
  "priK x"  == "invKey(pubK x)"
paulson@2318
    21
paulson@2318
    22
primrec initState agent
paulson@2318
    23
        (*Agents know their private key and all public keys*)
paulson@3519
    24
  initState_Server  "initState Server     =    
paulson@2318
    25
 		         insert (Key (priK Server)) (Key `` range pubK)"
paulson@3519
    26
  initState_Friend  "initState (Friend i) =    
paulson@2318
    27
 		         insert (Key (priK (Friend i))) (Key `` range pubK)"
paulson@3519
    28
  initState_Spy     "initState Spy        =    
paulson@3683
    29
 		         (Key``invKey``pubK``bad) Un (Key `` range pubK)"
paulson@2318
    30
paulson@2318
    31
paulson@2318
    32
rules
paulson@2318
    33
  (*Public keys are disjoint, and never clash with private keys*)
paulson@2451
    34
  inj_pubK        "inj pubK"
paulson@2451
    35
  priK_neq_pubK   "priK A ~= pubK B"
paulson@2318
    36
paulson@2318
    37
end