isabelle: src/HOL/Auth/Public.thy@44e57a6d947d (annotated)

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)
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

author	wenzelm
	Fri, 19 Dec 1997 12:09:58 +0100
changeset 4456	44e57a6d947d
parent 3683	aafe719dff14
child 5183	89f162de39cf
permissions	-rw-r--r--