doc-src/TutorialI/Protocol/Public.thy
author haftmann
Fri Jun 17 16:12:49 2005 +0200 (2005-06-17)
changeset 16417 9bc16273c2d4
parent 11250 c8bbf4c4bc2d
child 23925 ee98c2528a8f
permissions -rw-r--r--
migrated theory headers to new format
paulson@11250
     1
(*  Title:      HOL/Auth/Public
paulson@11250
     2
    ID:         $Id$
paulson@11250
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@11250
     4
    Copyright   1996  University of Cambridge
paulson@11250
     5
paulson@11250
     6
Theory of Public Keys (common to all public-key protocols)
paulson@11250
     7
paulson@11250
     8
Private and public keys; initial states of agents
paulson@11250
     9
*)
paulson@11250
    10
haftmann@16417
    11
theory Public imports Event
haftmann@16417
    12
uses ("Public_lemmas.ML") begin
paulson@11250
    13
paulson@11250
    14
consts
paulson@11250
    15
  pubK    :: "agent => key"
paulson@11250
    16
paulson@11250
    17
syntax
paulson@11250
    18
  priK    :: "agent => key"
paulson@11250
    19
paulson@11250
    20
translations  (*BEWARE! expressions like  (inj priK)  will NOT work!*)
paulson@11250
    21
  "priK x"  == "invKey(pubK x)"
paulson@11250
    22
paulson@11250
    23
primrec
paulson@11250
    24
        (*Agents know their private key and all public keys*)
paulson@11250
    25
  initState_Server:  "initState Server     =    
paulson@11250
    26
 		         insert (Key (priK Server)) (Key ` range pubK)"
paulson@11250
    27
  initState_Friend:  "initState (Friend i) =    
paulson@11250
    28
 		         insert (Key (priK (Friend i))) (Key ` range pubK)"
paulson@11250
    29
  initState_Spy:     "initState Spy        =    
paulson@11250
    30
 		         (Key`invKey`pubK`bad) Un (Key ` range pubK)"
paulson@11250
    31
paulson@11250
    32
paulson@11250
    33
axioms
paulson@11250
    34
  (*Public keys are disjoint, and never clash with private keys*)
paulson@11250
    35
  inj_pubK:        "inj pubK"
paulson@11250
    36
  priK_neq_pubK:   "priK A ~= pubK B"
paulson@11250
    37
paulson@11250
    38
use "Public_lemmas.ML"
paulson@11250
    39
paulson@11250
    40
(*Specialized methods*)
paulson@11250
    41
paulson@11250
    42
method_setup possibility = {*
paulson@11250
    43
    Method.no_args (Method.METHOD (fn facts => possibility_tac)) *}
paulson@11250
    44
    "for proving possibility theorems"
paulson@11250
    45
paulson@11250
    46
end