src/HOL/Auth/Public.thy
author paulson
Fri Jul 04 17:34:55 1997 +0200 (1997-07-04)
changeset 3500 0d8ad2f192d8
parent 3478 770939fecbb3
child 3512 9dcb4daa15e8
permissions -rw-r--r--
New constant "certificate"--just an abbreviation
     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 symmetric-key protocols)
     7 
     8 Server keys; initial states of agents; new nonces and keys; function "sees" 
     9 *)
    10 
    11 Public = Message + List + 
    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 consts  (*Initial states of agents -- parameter of the construction*)
    23   initState :: [agent set, agent] => msg set
    24 
    25 primrec initState agent
    26         (*Agents know their private key and all public keys*)
    27   initState_Server  "initState lost Server     =    
    28  		         insert (Key (priK Server)) (Key `` range pubK)"
    29   initState_Friend  "initState lost (Friend i) =    
    30  		         insert (Key (priK (Friend i))) (Key `` range pubK)"
    31   initState_Spy     "initState lost Spy        =    
    32  		         (Key``invKey``pubK``lost) Un (Key `` range pubK)"
    33 
    34 
    35 datatype  (*Messages, and components of agent stores*)
    36   event = Says agent agent msg
    37 
    38 consts  
    39   sees1 :: [agent, event] => msg set
    40 
    41 primrec sees1 event
    42            (*Spy reads all traffic whether addressed to him or not*)
    43   sees1_Says  "sees1 A (Says A' B X)  = (if A:{B,Spy} then {X} else {})"
    44 
    45 consts  
    46   sees :: [agent set, agent, event list] => msg set
    47 
    48 primrec sees list
    49   sees_Nil  "sees lost A []       = initState lost A"
    50   sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs"
    51 
    52 
    53 constdefs
    54   (*Set of items that might be visible to somebody: complement of the set
    55         of fresh items*)
    56   used :: event list => msg set
    57     "used evs == parts (UN lost B. sees lost B evs)"
    58 
    59 
    60 rules
    61   (*Public keys are disjoint, and never clash with private keys*)
    62   inj_pubK        "inj pubK"
    63   priK_neq_pubK   "priK A ~= pubK B"
    64 
    65 end