src/HOL/Auth/Public.thy
author paulson
Fri, 11 Jul 1997 13:26:15 +0200
changeset 3512 9dcb4daa15e8
parent 3478 770939fecbb3
child 3519 ab0a9fbed4c0
permissions -rw-r--r--
Moving common declarations and proofs from theories "Shared" and "Public" to "Event". NB the original "Event" theory was later renamed "Shared". Addition of the Notes constructor to datatype "event".
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Auth/Public
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
     2
    ID:         $Id$
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
     4
    Copyright   1996  University of Cambridge
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
     5
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3478
diff changeset
     6
Theory of Public Keys (common to all public-key protocols)
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
     7
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3478
diff changeset
     8
Private and public keys; initial states of agents
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
     9
*)
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    10
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents: 3478
diff changeset
    11
Public = Event + 
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    12
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    13
consts
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    14
  pubK    :: agent => key
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    15
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    16
syntax
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    17
  priK    :: agent => key
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    18
3478
770939fecbb3 Removal of the obsolete newN function
paulson
parents: 2497
diff changeset
    19
translations  (*BEWARE! expressions like  (inj priK)  will NOT work!*)
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    20
  "priK x"  == "invKey(pubK x)"
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    21
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    22
primrec initState agent
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    23
        (*Agents know their private key and all public keys*)
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    24
  initState_Server  "initState lost Server     =    
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    25
 		         insert (Key (priK Server)) (Key `` range pubK)"
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    26
  initState_Friend  "initState lost (Friend i) =    
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    27
 		         insert (Key (priK (Friend i))) (Key `` range pubK)"
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    28
  initState_Spy     "initState lost Spy        =    
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    29
 		         (Key``invKey``pubK``lost) Un (Key `` range pubK)"
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    30
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    31
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    32
rules
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    33
  (*Public keys are disjoint, and never clash with private keys*)
2451
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2318
diff changeset
    34
  inj_pubK        "inj pubK"
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2318
diff changeset
    35
  priK_neq_pubK   "priK A ~= pubK B"
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    36
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    37
end