isabelle: src/HOL/Auth/Public.thy@0103ee3082bf (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
11104 f2024fed9f0c partial conversion to Isar script style paulson parents: 10833 diff changeset	11	theory Public = Event
f2024fed9f0c partial conversion to Isar script style paulson parents: 10833 diff changeset	12	files ("Public_lemmas.ML"):
2318 6d3f7c7f70b0 Public-key examples paulson parents: diff changeset	13
6d3f7c7f70b0 Public-key examples paulson parents: diff changeset	14	consts
11104 f2024fed9f0c partial conversion to Isar script style paulson parents: 10833 diff changeset	15	pubK :: "agent => key"
2318 6d3f7c7f70b0 Public-key examples paulson parents: diff changeset	16
6d3f7c7f70b0 Public-key examples paulson parents: diff changeset	17	syntax
11104 f2024fed9f0c partial conversion to Isar script style paulson parents: 10833 diff changeset	18	priK :: "agent => key"
2318 6d3f7c7f70b0 Public-key examples paulson parents: diff changeset	19
3478 770939fecbb3 Removal of the obsolete newN function paulson parents: 2497 diff changeset	20	translations (BEWARE! expressions like (inj priK) will NOT work!)
2318 6d3f7c7f70b0 Public-key examples paulson parents: diff changeset	21	"priK x" == "invKey(pubK x)"
6d3f7c7f70b0 Public-key examples paulson parents: diff changeset	22
5183 89f162de39cf Adapted to new datatype package. berghofe parents: 3683 diff changeset	23	primrec
2318 6d3f7c7f70b0 Public-key examples paulson parents: diff changeset	24	(Agents know their private key and all public keys)
11104 f2024fed9f0c partial conversion to Isar script style paulson parents: 10833 diff changeset	25	initState_Server: "initState Server =
10833 c0844a30ea4e `` -> ` and ``` -> `` nipkow parents: 5183 diff changeset	26	insert (Key (priK Server)) (Key ` range pubK)"
11104 f2024fed9f0c partial conversion to Isar script style paulson parents: 10833 diff changeset	27	initState_Friend: "initState (Friend i) =
10833 c0844a30ea4e `` -> ` and ``` -> `` nipkow parents: 5183 diff changeset	28	insert (Key (priK (Friend i))) (Key ` range pubK)"
11104 f2024fed9f0c partial conversion to Isar script style paulson parents: 10833 diff changeset	29	initState_Spy: "initState Spy =
10833 c0844a30ea4e `` -> ` and ``` -> `` nipkow parents: 5183 diff changeset	30	(Key`invKey`pubK`bad) Un (Key ` range pubK)"
2318 6d3f7c7f70b0 Public-key examples paulson parents: diff changeset	31
6d3f7c7f70b0 Public-key examples paulson parents: diff changeset	32
11104 f2024fed9f0c partial conversion to Isar script style paulson parents: 10833 diff changeset	33	axioms
2318 6d3f7c7f70b0 Public-key examples paulson parents: diff changeset	34	(Public keys are disjoint, and never clash with private keys)
11104 f2024fed9f0c partial conversion to Isar script style paulson parents: 10833 diff changeset	35	inj_pubK: "inj pubK"
f2024fed9f0c partial conversion to Isar script style paulson parents: 10833 diff changeset	36	priK_neq_pubK: "priK A ~= pubK B"
f2024fed9f0c partial conversion to Isar script style paulson parents: 10833 diff changeset	37
f2024fed9f0c partial conversion to Isar script style paulson parents: 10833 diff changeset	38	use "Public_lemmas.ML"
f2024fed9f0c partial conversion to Isar script style paulson parents: 10833 diff changeset	39
11287 0103ee3082bf conversion of Auth/TLS to Isar script paulson parents: 11270 diff changeset	40	lemma [simp]: "K \\<in> symKeys ==> invKey K = K"
0103ee3082bf conversion of Auth/TLS to Isar script paulson parents: 11270 diff changeset	41	by (simp add: symKeys_def)
0103ee3082bf conversion of Auth/TLS to Isar script paulson parents: 11270 diff changeset	42
11104 f2024fed9f0c partial conversion to Isar script style paulson parents: 10833 diff changeset	43	(Specialized methods)
f2024fed9f0c partial conversion to Isar script style paulson parents: 10833 diff changeset	44
f2024fed9f0c partial conversion to Isar script style paulson parents: 10833 diff changeset	45	method_setup possibility = {*
11270 a315a3862bb4 better treatment of methods: uses Method.ctxt_args to refer to current paulson parents: 11104 diff changeset	46	Method.ctxt_args (fn ctxt =>
a315a3862bb4 better treatment of methods: uses Method.ctxt_args to refer to current paulson parents: 11104 diff changeset	47	Method.METHOD (fn facts =>
a315a3862bb4 better treatment of methods: uses Method.ctxt_args to refer to current paulson parents: 11104 diff changeset	48	gen_possibility_tac (Simplifier.get_local_simpset ctxt))) *}
11104 f2024fed9f0c partial conversion to Isar script style paulson parents: 10833 diff changeset	49	"for proving possibility theorems"
2318 6d3f7c7f70b0 Public-key examples paulson parents: diff changeset	50
6d3f7c7f70b0 Public-key examples paulson parents: diff changeset	51	end

author	paulson
	Tue, 08 May 2001 15:56:57 +0200
changeset 11287	0103ee3082bf
parent 11270	a315a3862bb4
child 13922	75ae4244a596
permissions	-rw-r--r--