equal
deleted
inserted
replaced
14 Cambridge CB3 0FD, United Kingdom |
14 Cambridge CB3 0FD, United Kingdom |
15 ******************************************************************************) |
15 ******************************************************************************) |
16 |
16 |
17 header{*protocol-independent confidentiality theorem on keys*} |
17 header{*protocol-independent confidentiality theorem on keys*} |
18 |
18 |
19 theory GuardK = Analz + Extensions: |
19 theory GuardK imports Analz Extensions begin |
20 |
20 |
21 (****************************************************************************** |
21 (****************************************************************************** |
22 messages where all the occurrences of Key n are |
22 messages where all the occurrences of Key n are |
23 in a sub-message of the form Crypt (invKey K) X with K:Ks |
23 in a sub-message of the form Crypt (invKey K) X with K:Ks |
24 ******************************************************************************) |
24 ******************************************************************************) |