src/HOL/Auth/Shared.thy
changeset 3414 804c8a178a7f
parent 2516 4d68fbe6378b
child 3472 fb3c38c88c08
equal deleted inserted replaced
3413:c1f63cc3a768 3414:804c8a178a7f
    57     We have infinitely many agents and there is nothing to stop their
    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
    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
    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
    60     many fresh session keys.  We could, alternatively, restrict agents to
    61     an unspecified finite number.*)
    61     an unspecified finite number.*)
    62   Key_supply_ax  "KK: Fin UNIV ==> EX K. K ~: KK & Key K ~: used evs"
    62   Key_supply_ax  "finite KK ==> EX K. K ~: KK & Key K ~: used evs"
    63 
    63 
    64 
    64 
    65 (*Agents generate random (symmetric) keys and nonces.
    65 (*Agents generate random (symmetric) keys and nonces.
    66   The numeric argument is typically the length of the current trace.
    66   The numeric argument is typically the length of the current trace.
    67   An injective pairing function allows multiple keys/nonces to be generated
    67   An injective pairing function allows multiple keys/nonces to be generated