isabelle: src/HOL/Auth/Public.thy@c0844a30ea4e (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
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 =
10833 c0844a30ea4e `` -> ` and ``` -> `` nipkow parents: 5183 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) =
10833 c0844a30ea4e `` -> ` and ``` -> `` nipkow parents: 5183 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 =
10833 c0844a30ea4e `` -> ` and ``` -> `` nipkow parents: 5183 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	nipkow
	Tue, 09 Jan 2001 15:29:17 +0100
changeset 10833	c0844a30ea4e
parent 5183	89f162de39cf
child 11104	f2024fed9f0c
permissions	-rw-r--r--