equal
deleted
inserted
replaced
8 |
8 |
9 theory Recur imports Public begin |
9 theory Recur imports Public begin |
10 |
10 |
11 text{*End marker for message bundles*} |
11 text{*End marker for message bundles*} |
12 abbreviation |
12 abbreviation |
13 END :: "msg" |
13 END :: "msg" where |
14 "END == Number 0" |
14 "END == Number 0" |
15 |
15 |
16 (*Two session keys are distributed to each agent except for the initiator, |
16 (*Two session keys are distributed to each agent except for the initiator, |
17 who receives one. |
17 who receives one. |
18 Perhaps the two session keys could be bundled into a single message. |
18 Perhaps the two session keys could be bundled into a single message. |