equal
deleted
inserted
replaced
1 (* Title: HOL/Auth/Public |
1 (* Title: HOL/Auth/Public |
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1996 University of Cambridge |
3 Copyright 1996 University of Cambridge |
5 |
4 |
6 Theory of Public Keys (common to all public-key protocols) |
5 Theory of Public Keys (common to all public-key protocols) |
7 |
6 |
8 Private and public keys; initial states of agents |
7 Private and public keys; initial states of agents |
9 *) |
8 *) |
10 |
9 |
11 theory Public imports Event begin |
10 theory Public |
|
11 imports Event |
|
12 begin |
12 |
13 |
13 lemma invKey_K: "K \<in> symKeys ==> invKey K = K" |
14 lemma invKey_K: "K \<in> symKeys ==> invKey K = K" |
14 by (simp add: symKeys_def) |
15 by (simp add: symKeys_def) |
15 |
16 |
16 subsection{*Asymmetric Keys*} |
17 subsection{*Asymmetric Keys*} |