isabelle: src/HOL/Auth/Shared.thy@3087dafb70ec (annotated)

1934 58573e7041b4 Separation of theory Event into two parts: paulson parents: diff changeset	1	(* Title: HOL/Auth/Shared
58573e7041b4 Separation of theory Event into two parts: paulson parents: diff changeset	2	ID: $Id$
58573e7041b4 Separation of theory Event into two parts: paulson parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
58573e7041b4 Separation of theory Event into two parts: paulson parents: diff changeset	4	Copyright 1996 University of Cambridge
58573e7041b4 Separation of theory Event into two parts: paulson parents: diff changeset	5
58573e7041b4 Separation of theory Event into two parts: paulson parents: diff changeset	6	Theory of Shared Keys (common to all symmetric-key protocols)
58573e7041b4 Separation of theory Event into two parts: paulson parents: diff changeset	7
3512 9dcb4daa15e8 Moving common declarations and proofs from theories "Shared" paulson parents: 3472 diff changeset	8	Shared, long-term keys; initial states of agents
1934 58573e7041b4 Separation of theory Event into two parts: paulson parents: diff changeset	9	*)
58573e7041b4 Separation of theory Event into two parts: paulson parents: diff changeset	10
3512 9dcb4daa15e8 Moving common declarations and proofs from theories "Shared" paulson parents: 3472 diff changeset	11	Shared = Event + Finite +
1934 58573e7041b4 Separation of theory Event into two parts: paulson parents: diff changeset	12
58573e7041b4 Separation of theory Event into two parts: paulson parents: diff changeset	13	consts
1943 20574dca5a3e Renaming and simplification paulson parents: 1934 diff changeset	14	shrK :: agent => key (symmetric keys)
1967 0ff58b41c037 "bad" set simplifies statements of many theorems paulson parents: 1965 diff changeset	15
1934 58573e7041b4 Separation of theory Event into two parts: paulson parents: diff changeset	16	rules
3472 fb3c38c88c08 Deleted the obsolete operators newK, newN and nPair paulson parents: 3414 diff changeset	17	isSym_keys "isSymKey K" (All keys are symmetric)
fb3c38c88c08 Deleted the obsolete operators newK, newN and nPair paulson parents: 3414 diff changeset	18	inj_shrK "inj shrK" (No two agents have the same long-term key)
1934 58573e7041b4 Separation of theory Event into two parts: paulson parents: diff changeset	19
5183 89f162de39cf Adapted to new datatype package. berghofe parents: 3683 diff changeset	20	primrec
2319 95f0d5243c85 Updating of comments paulson parents: 2264 diff changeset	21	(Server knows all long-term keys; other agents know only their own)
3519 ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant. paulson parents: 3512 diff changeset	22	initState_Server "initState Server = Key `` range shrK"
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant. paulson parents: 3512 diff changeset	23	initState_Friend "initState (Friend i) = {Key (shrK (Friend i))}"
3683 aafe719dff14 Global change: lost->bad and sees Spy->spies paulson parents: 3519 diff changeset	24	initState_Spy "initState Spy = Key``shrK``bad"
2032 1bbf1bdcaf56 Introduction of "lost" argument paulson parents: 2012 diff changeset	25
1934 58573e7041b4 Separation of theory Event into two parts: paulson parents: diff changeset	26
2516 4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K paulson parents: 2451 diff changeset	27	rules
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K paulson parents: 2451 diff changeset	28	(*Unlike the corresponding property of nonces, this cannot be proved.
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K paulson parents: 2451 diff changeset	29	We have infinitely many agents and there is nothing to stop their
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K paulson parents: 2451 diff changeset	30	long-term keys from exhausting all the natural numbers. The axiom
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K paulson parents: 2451 diff changeset	31	assumes that their keys are dispersed so as to leave room for infinitely
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K paulson parents: 2451 diff changeset	32	many fresh session keys. We could, alternatively, restrict agents to
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K paulson parents: 2451 diff changeset	33	an unspecified finite number.*)
3414 804c8a178a7f Modified a few defs and proofs because of the changes to theory Finite.thy. nipkow parents: 2516 diff changeset	34	Key_supply_ax "finite KK ==> EX K. K ~: KK & Key K ~: used evs"
2516 4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K paulson parents: 2451 diff changeset	35
1934 58573e7041b4 Separation of theory Event into two parts: paulson parents: diff changeset	36	end

author	paulson
	Tue, 04 Aug 1998 16:06:55 +0200
changeset 5242	3087dafb70ec
parent 5183	89f162de39cf
child 10833	c0844a30ea4e
permissions	-rw-r--r--