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

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 |