equal
deleted
inserted
replaced
12 declare initState.simps [simp del] |
12 declare initState.simps [simp del] |
13 |
13 |
14 subsubsection\<open>signature\<close> |
14 subsubsection\<open>signature\<close> |
15 |
15 |
16 definition sign :: "agent => msg => msg" where |
16 definition sign :: "agent => msg => msg" where |
17 "sign A X == {|Agent A, X, Crypt (priK A) (Hash X)|}" |
17 "sign A X == \<lbrace>Agent A, X, Crypt (priK A) (Hash X)\<rbrace>" |
18 |
18 |
19 lemma sign_inj [iff]: "(sign A X = sign A' X') = (A=A' & X=X')" |
19 lemma sign_inj [iff]: "(sign A X = sign A' X') = (A=A' & X=X')" |
20 by (auto simp: sign_def) |
20 by (auto simp: sign_def) |
21 |
21 |
22 subsubsection\<open>agent associated to a key\<close> |
22 subsubsection\<open>agent associated to a key\<close> |