Re: [isabelle] HOL/Auth subgoal (Nonce secrecy)



Larry/Denis

	I think the problem here has to do with the proof strategy you are taking. It is not unusual you ending up with these complications (double insert inside an analz) if you are too aggressive at the beginning of the proof. Larry's reading recommendation can be complemented by chapter 4 in Giampaolo Bella's book.

	If you want to post privately the entire lemma and the proof commands you written so far I can take a look to see if it is one of the usuals.

Regards,

Jean


On 12 Oct 2010, at 10:25, Lawrence Paulson wrote:

> Any theorem involving the function analz requires special care. As you say, this one is conceptually trivial because all the information being added to the spy's knowledge is already publicly available. But you still have to go about the proof in the right way.
> 
> This subgoal appears to be unsimplified. The standard setup of simplification rules for analz is designed to deal with this sort of term. They permute the inserted items so that trivial ones (such as agent names) are called to the front and then taken outside of the analz call altogether. So try 
> 
> apply (simp add: analz_insert_eq pushes split_ifs)
> 
> You should be left with nothing but the key. For a secrecy theorem, dealing with the key is complicated, and you need to use some of the measures outlined in section 4.5 of my paper “The Inductive Approach to Verifying Cryptographic Protocols”. But because this is a public key, you should only need to use the theorem Set.insert_absorb to erase it. In fact you probably won't need this final step, because analz_insert_eq above should take care of it. Good luck!
> 
> Larry Paulson
> 
> 
> On 11 Oct 2010, at 20:01, Denis Butin wrote:
> 
>> Hi all,
>> 
>> I am using the security protocol framework from HOL/Auth, and I am
>> frustratingly stuck on the following subgoal:
>> 
>>       [A \<notin> bad; R \<notin> bad;
>>        evsp1 \<in> ns_public_pki;
>>       Says A B (Crypt (pubK R) {Nonce NC, Agent A}) \<in> set evsp1;
>>       Nonce NC \<notin> analz (knows Spy evsp1);
>>       Nonce NC \<in> analz (insert (Key (pubK Aa)) (insert {Agent
>> Aa, Number certa} (knows Spy evsp1)))]
>> 
>>     ==> False
>> 
>> It seems easy: I just have to show that adding a public key, an
>> agent's name and a number to the Spy's knowledge doesn't change the
>> secrecy of the nonce NC, which leads to the required contradiction.
>> 
>> The following lemmas seem helpful:
>> - privateKey_neq_publicKey (a private key can never be a public key,
>> hence pubK Aa cannot be the inverse of pubK R) ;
>> - parts_insert_spies ( parts (insert ?X (knows Spy ?evs)) = parts {?X}
>> \<union> parts (knows Spy ?evs));
>> - analz_into_parts, which is already declared as [dest] at the
>> beginning of my theory;
>> - knows_Cons, which is part of the inductive definition of the knows function.
>> 
>> My only problem is how to put them together; I unsuccessfuly tried things like
>> 
>> apply (auto intro: privateKey_neq_publicKey knows_Cons simp add:
>> parts_insert_spies)
>> 
>> I am not too sure on the best way to use/combine auto or blast with
>> existing lemmas, so I may have missed something obvious.
>> 
>> Sledgehammer suggested a metis command which resulted in an Ill-typed
>> instantiation error.
>> 
>> Many thanks for reading this, and for any help.
>> 
>> Regards,
>> Denis
>> 
> 
> 






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.