41 lemma Nonce_in_chain [iff]: "Nonce ofr:parts {chain B ofr A L C}" |
41 lemma Nonce_in_chain [iff]: "Nonce ofr:parts {chain B ofr A L C}" |
42 by (auto simp: chain_def sign_def) |
42 by (auto simp: chain_def sign_def) |
43 |
43 |
44 subsubsection{*agent whose key is used to sign an offer*} |
44 subsubsection{*agent whose key is used to sign an offer*} |
45 |
45 |
46 consts shop :: "msg => msg" |
46 fun shop :: "msg => msg" where |
47 |
|
48 recdef shop "measure size" |
|
49 "shop {|Crypt K {|B,ofr,Crypt K' H|},m2|} = Agent (agt K')" |
47 "shop {|Crypt K {|B,ofr,Crypt K' H|},m2|} = Agent (agt K')" |
50 |
48 |
51 lemma shop_chain [simp]: "shop (chain B ofr A L C) = Agent B" |
49 lemma shop_chain [simp]: "shop (chain B ofr A L C) = Agent B" |
52 by (simp add: chain_def sign_def) |
50 by (simp add: chain_def sign_def) |
53 |
51 |
54 subsubsection{*nonce used in an offer*} |
52 subsubsection{*nonce used in an offer*} |
55 |
53 |
56 consts nonce :: "msg => msg" |
54 fun nonce :: "msg => msg" where |
57 |
|
58 recdef nonce "measure size" |
|
59 "nonce {|Crypt K {|B,ofr,CryptH|},m2|} = ofr" |
55 "nonce {|Crypt K {|B,ofr,CryptH|},m2|} = ofr" |
60 |
56 |
61 lemma nonce_chain [simp]: "nonce (chain B ofr A L C) = Nonce ofr" |
57 lemma nonce_chain [simp]: "nonce (chain B ofr A L C) = Nonce ofr" |
62 by (simp add: chain_def sign_def) |
58 by (simp add: chain_def sign_def) |
63 |
59 |
64 subsubsection{*next shop*} |
60 subsubsection{*next shop*} |
65 |
61 |
66 consts next_shop :: "msg => agent" |
62 fun next_shop :: "msg => agent" where |
67 |
|
68 recdef next_shop "measure size" |
|
69 "next_shop {|m1,Hash {|headL,Agent C|}|} = C" |
63 "next_shop {|m1,Hash {|headL,Agent C|}|} = C" |
70 |
64 |
71 lemma "next_shop (chain B ofr A L C) = C" |
65 lemma "next_shop (chain B ofr A L C) = C" |
72 by (simp add: chain_def sign_def) |
66 by (simp add: chain_def sign_def) |
73 |
67 |
162 lemma valid_pos_len: "L:valid A n B ==> 0 < len L" |
156 lemma valid_pos_len: "L:valid A n B ==> 0 < len L" |
163 by (erule valid.induct, auto) |
157 by (erule valid.induct, auto) |
164 |
158 |
165 subsubsection{*list of offers*} |
159 subsubsection{*list of offers*} |
166 |
160 |
167 consts offers :: "msg => msg" |
161 fun offers :: "msg => msg" |
168 |
162 where |
169 recdef offers "measure size" |
163 "offers (cons M L) = cons {|shop M, nonce M|} (offers L)" |
170 "offers (cons M L) = cons {|shop M, nonce M|} (offers L)" |
164 | "offers other = nil" |
171 "offers other = nil" |
|
172 |
165 |
173 |
166 |
174 subsection{*Properties of Protocol P2*} |
167 subsection{*Properties of Protocol P2*} |
175 |
168 |
176 text{*same as @{text P1_Prop} except that publicly verifiable forward |
169 text{*same as @{text P1_Prop} except that publicly verifiable forward |