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.
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
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 3683
diff changeset
    22
primrec
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    23
        (*Agents know their private key and all public keys*)
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3512
diff changeset
    24
  initState_Server  "initState Server     =    
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    25
 		         insert (Key (priK Server)) (Key `` range pubK)"
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3512
diff changeset
    26
  initState_Friend  "initState (Friend i) =    
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    27
 		         insert (Key (priK (Friend i))) (Key `` range pubK)"
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3512
diff changeset
    28
  initState_Spy     "initState Spy        =    
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3519
diff changeset
    29
 		         (Key``invKey``pubK``bad) Un (Key `` range pubK)"
2318
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