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

src/HOL/Auth/Shared.thy

author | nipkow |

Thu Jun 05 14:40:35 1997 +0200 (1997-06-05) | |

changeset 3414 | 804c8a178a7f |

parent 2516 | 4d68fbe6378b |

child 3472 | fb3c38c88c08 |

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

Modified a few defs and proofs because of the changes to theory Finite.thy.

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 Server keys; initial states of agents; new nonces and keys; function "sees"

9 *)

11 Shared = Message + List + Finite +

13 consts

14 shrK :: agent => key (*symmetric keys*)

16 rules

17 (*ALL keys are symmetric*)

18 isSym_keys "isSymKey K"

20 consts (*Initial states of agents -- parameter of the construction*)

21 initState :: [agent set, agent] => msg set

23 primrec initState agent

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

25 initState_Server "initState lost Server = Key `` range shrK"

26 initState_Friend "initState lost (Friend i) = {Key (shrK (Friend i))}"

27 initState_Spy "initState lost Spy = Key``shrK``lost"

30 datatype (*Messages, and components of agent stores*)

31 event = Says agent agent msg

33 consts

34 sees1 :: [agent, event] => msg set

36 primrec sees1 event

37 (*Spy reads all traffic whether addressed to him or not*)

38 sees1_Says "sees1 A (Says A' B X) = (if A:{B,Spy} then {X} else {})"

40 consts

41 sees :: [agent set, agent, event list] => msg set

43 primrec sees list

44 sees_Nil "sees lost A [] = initState lost A"

45 sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs"

48 constdefs

49 (*Set of items that might be visible to somebody: complement of the set

50 of fresh items*)

51 used :: event list => msg set

52 "used evs == parts (UN lost B. sees lost B evs)"

55 rules

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

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

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

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

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

61 an unspecified finite number.*)

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

65 (*Agents generate random (symmetric) keys and nonces.

66 The numeric argument is typically the length of the current trace.

67 An injective pairing function allows multiple keys/nonces to be generated

68 in one protocol round. A typical candidate for npair(i,j) is

69 2^j(2i+1)

70 *)

72 consts

73 nPair :: "nat*nat => nat"

74 newN :: "nat => nat"

75 newK :: "nat => key"

77 rules

78 inj_shrK "inj shrK"

79 inj_nPair "inj nPair"

80 inj_newN "inj newN"

81 inj_newK "inj newK"

83 newK_neq_shrK "newK i ~= shrK A"

85 end