summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Auth/Shared.thy

author | paulson |

Mon, 14 Jul 1997 12:47:21 +0200 | |

changeset 3519 | ab0a9fbed4c0 |

parent 3512 | 9dcb4daa15e8 |

child 3683 | aafe719dff14 |

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

Changing "lost" from a parameter of protocol definitions to a constant.
Advantages: no "lost" argument everywhere; fewer Vars in subgoals;
less need for specially instantiated rules
Disadvantage: can no longer prove "Agent_not_see_encrypted_key", but this
theorem was never used, and its original proof was also broken
the introduction of the "Notes" constructor.

(* Title: HOL/Auth/Shared ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1996 University of Cambridge Theory of Shared Keys (common to all symmetric-key protocols) Shared, long-term keys; initial states of agents *) Shared = Event + Finite + consts shrK :: agent => key (*symmetric keys*) rules isSym_keys "isSymKey K" (*All keys are symmetric*) inj_shrK "inj shrK" (*No two agents have the same long-term key*) primrec initState agent (*Server knows all long-term keys; other agents know only their own*) initState_Server "initState Server = Key `` range shrK" initState_Friend "initState (Friend i) = {Key (shrK (Friend i))}" initState_Spy "initState Spy = Key``shrK``lost" rules (*Unlike the corresponding property of nonces, this cannot be proved. We have infinitely many agents and there is nothing to stop their long-term keys from exhausting all the natural numbers. The axiom assumes that their keys are dispersed so as to leave room for infinitely many fresh session keys. We could, alternatively, restrict agents to an unspecified finite number.*) Key_supply_ax "finite KK ==> EX K. K ~: KK & Key K ~: used evs" end