1 (****************************************************************************** |
1 (* Title: HOL/Auth/Guard/GuardK.thy |
2 very similar to Guard except: |
2 Author: Frederic Blanqui, University of Cambridge Computer Laboratory |
|
3 Copyright 2002 University of Cambridge |
|
4 |
|
5 Very similar to Guard except: |
3 - Guard is replaced by GuardK, guard by guardK, Nonce by Key |
6 - Guard is replaced by GuardK, guard by guardK, Nonce by Key |
4 - some scripts are slightly modified (+ keyset_in, kparts_parts) |
7 - some scripts are slightly modified (+ keyset_in, kparts_parts) |
5 - the hypothesis Key n ~:G (keyset G) is added |
8 - the hypothesis Key n ~:G (keyset G) is added |
6 |
9 *) |
7 date: march 2002 |
|
8 author: Frederic Blanqui |
|
9 email: blanqui@lri.fr |
|
10 webpage: http://www.lri.fr/~blanqui/ |
|
11 |
|
12 University of Cambridge, Computer Laboratory |
|
13 William Gates Building, JJ Thomson Avenue |
|
14 Cambridge CB3 0FD, United Kingdom |
|
15 ******************************************************************************) |
|
16 |
10 |
17 header{*protocol-independent confidentiality theorem on keys*} |
11 header{*protocol-independent confidentiality theorem on keys*} |
18 |
12 |
19 theory GuardK |
13 theory GuardK |
20 imports Analz Extensions |
14 imports Analz Extensions |