[Verifpal] Missed trivial attack

[Nadim Kobeissi]

To be more precise about the current situation: Verifpal currently does not inject new primitive-type values as an active attacker. This functionality is currently being rewritten from scratch to take into account the rewrite of some parts of the analysis logic in 0.6.8.

Therefore, this and any similar models that require the attacker to inject primitives that it invents won’t work properly.

I’m actually really excited about this, because I’ve been able to get some strong confidence on the correctness of Verifpal’s behavior outside of the injection of primitives specifically, and think we’ll be in very good shape once that latter part is rewritten.

Nadim Kobeissi
Symbolic Software • https://symbolic.software

> On Sep 18, 2019, at 9:34 PM, Nadim Kobeissi <nadim at symbolic.software> wrote:
> 
> Not at all surprising, this is what I was talking about when I said that I was sure 0.6.8 would miss attacks. I’m working on resolving similar scenarios.
> 
> Verifpal should be considered under heavy refactoring until 0.7.
> 
> Nadim Kobeissi
> Symbolic Software • https://symbolic.software
> 
>> On Sep 18, 2019, at 9:30 PM, Loup Vaillant David <loup at loup-vaillant.fr> wrote:
>> 
>> (Originally sent to Nadim only, sorry for the duplicate.)
>> 
>> Hi,
>> 
>> I have a little problem with this Model:
>> 
>>   attacker [active]
>>   principal Alice [ generates e ]
>>   principal Bob   [             ]
>>   Alice -> Bob: e
>>   principal Bob   [ H = HASH(e) ]
>> 
>>   queries [
>>       authentication? Alice -> Bob : e
>>   ]
>> 
>> The latest commit from the master branch (b3dd726), finds no result.
>> Yet `e` here is successfully used in HASH(e), right?
>> 
>> ---
>> 
>> I found this trying to build a minimum failing test case for Monokex. I
>> figured the recipient could not authenticate anything, because the
>> initiator never sent them any public key (not static, not ephemeral)
>> over a secure channel. Then there's the little problem of sending the
>> same thing twice, but making sure the second time is right:
>> 
>>   // before the protocol
>>   Alice -> Bob [public_key]
>> 
>>   // during the protocol
>>   Alice -> Bob public_key
>> 
>> In real world protocols, Bob compares the insecurely sent public key,
>> with the one he trusts. I'm not sure how we would model that in
>> Verifpal?
>> 
>> But first, there's this little issue.
>> 
>> Loup.
>> 
>> 
>> _______________________________________________
>> Verifpal mailing list
>> Verifpal at lists.symbolic.software
>> https://lists.symbolic.software/mailman/listinfo/verifpal
>