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

src/HOL/Auth/Shared.thy

author | paulson |

Wed Dec 24 10:02:30 1997 +0100 (1997-12-24) | |

changeset 4477 | b3e5857d8d99 |

parent 3683 | aafe719dff14 |

child 5183 | 89f162de39cf |

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

New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort

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 Shared = Event + Finite +

13 consts

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

16 rules

17 isSym_keys "isSymKey K" (*All keys are symmetric*)

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

20 primrec initState agent

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

22 initState_Server "initState Server = Key `` range shrK"

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

24 initState_Spy "initState Spy = Key``shrK``bad"

27 rules

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

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

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

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

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

33 an unspecified finite number.*)

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

36 end