summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Auth/Shared.thy

author | paulson |

Sat Aug 17 14:55:08 2002 +0200 (2002-08-17) | |

changeset 13507 | febb8e5d2a9d |

parent 12415 | 74977582a585 |

child 13907 | 2bc462b99e70 |

permissions | -rw-r--r-- |

tidying of Isar scripts

1 (* Title: HOL/Auth/Shared

2 ID: $Id$

3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory

4 Copyright 1996 University of Cambridge

6 Theory of Shared Keys (common to all symmetric-key protocols)

8 Shared, long-term keys; initial states of agents

9 *)

11 theory Shared = Event

12 files ("Shared_lemmas.ML"):

14 consts

15 shrK :: "agent => key" (*symmetric keys*)

17 axioms

18 isSym_keys: "K \<in> symKeys" (*All keys are symmetric*)

19 inj_shrK: "inj shrK" (*No two agents have the same long-term key*)

21 primrec

22 (*Server knows all long-term keys; other agents know only their own*)

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"

28 axioms

29 (*Unlike the corresponding property of nonces, this cannot be proved.

30 We have infinitely many agents and there is nothing to stop their

31 long-term keys from exhausting all the natural numbers. The axiom

32 assumes that their keys are dispersed so as to leave room for infinitely

33 many fresh session keys. We could, alternatively, restrict agents to

34 an unspecified finite number.*)

35 Key_supply_ax: "finite KK ==> EX K. K ~: KK & Key K ~: used evs"

37 use "Shared_lemmas.ML"

39 (*Lets blast_tac perform this step without needing the simplifier*)

40 lemma invKey_shrK_iff [iff]:

41 "(Key (invKey K) \<in> X) = (Key K \<in> X)"

42 by auto

44 (*Specialized methods*)

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"

54 method_setup possibility = {*

55 Method.ctxt_args (fn ctxt =>

56 Method.METHOD (fn facts =>

57 gen_possibility_tac (Simplifier.get_local_simpset ctxt))) *}

58 "for proving possibility theorems"

60 lemma knows_subset_knows_Cons: "knows A evs <= knows A (e # evs)"

61 by (induct e, auto simp: knows_Cons)

63 end