author | paulson |
Fri, 27 Apr 2001 17:16:21 +0200 | |
changeset 11270 | a315a3862bb4 |
parent 11230 | 756c5034f08b |
child 12415 | 74977582a585 |
permissions | -rw-r--r-- |
1934 | 1 |
(* Title: HOL/Auth/Shared |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1996 University of Cambridge |
|
5 |
||
6 |
Theory of Shared Keys (common to all symmetric-key protocols) |
|
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 | 9 |
*) |
10 |
||
11104 | 11 |
theory Shared = Event |
12 |
files ("Shared_lemmas.ML"): |
|
1934 | 13 |
|
14 |
consts |
|
11104 | 15 |
shrK :: "agent => key" (*symmetric keys*) |
1967 | 16 |
|
11104 | 17 |
axioms |
11270
a315a3862bb4
better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents:
11230
diff
changeset
|
18 |
isSym_keys: "K \<in> symKeys" (*All keys are symmetric*) |
11104 | 19 |
inj_shrK: "inj shrK" (*No two agents have the same long-term key*) |
1934 | 20 |
|
5183 | 21 |
primrec |
2319 | 22 |
(*Server knows all long-term keys; other agents know only their own*) |
11104 | 23 |
initState_Server: "initState Server = Key ` range shrK" |
24 |
initState_Friend: "initState (Friend i) = {Key (shrK (Friend i))}" |
|
25 |
initState_Spy: "initState Spy = Key`shrK`bad" |
|
2032 | 26 |
|
1934 | 27 |
|
11104 | 28 |
axioms |
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
29 |
(*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
|
30 |
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
|
31 |
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
|
32 |
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
|
33 |
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
|
34 |
an unspecified finite number.*) |
11104 | 35 |
Key_supply_ax: "finite KK ==> EX K. K ~: KK & Key K ~: used evs" |
36 |
||
37 |
use "Shared_lemmas.ML" |
|
38 |
||
39 |
(*Lets blast_tac perform this step without needing the simplifier*) |
|
40 |
lemma invKey_shrK_iff [iff]: |
|
11270
a315a3862bb4
better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents:
11230
diff
changeset
|
41 |
"(Key (invKey K) \<in> X) = (Key K \<in> X)" |
11104 | 42 |
by auto; |
43 |
||
44 |
(*Specialized methods*) |
|
45 |
||
46 |
method_setup analz_freshK = {* |
|
47 |
Method.no_args |
|
48 |
(Method.METHOD |
|
49 |
(fn facts => EVERY [REPEAT_FIRST (resolve_tac [allI, impI]), |
|
50 |
REPEAT_FIRST (rtac analz_image_freshK_lemma), |
|
51 |
ALLGOALS (asm_simp_tac analz_image_freshK_ss)])) *} |
|
52 |
"for proving the Session Key Compromise theorem" |
|
53 |
||
54 |
method_setup possibility = {* |
|
11270
a315a3862bb4
better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents:
11230
diff
changeset
|
55 |
Method.ctxt_args (fn ctxt => |
a315a3862bb4
better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents:
11230
diff
changeset
|
56 |
Method.METHOD (fn facts => |
a315a3862bb4
better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents:
11230
diff
changeset
|
57 |
gen_possibility_tac (Simplifier.get_local_simpset ctxt))) *} |
11104 | 58 |
"for proving possibility theorems" |
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
59 |
|
1934 | 60 |
end |