[Verifpal] New analysis with nil

[Nadim Kobeissi]

Dear jq-rs,

Thank you for your email and sorry for the late response.

I’ve looked briefly at your model and while I haven’t reverse engineered your entire protocol, I believe the issue likely has to do with the following:

DEC is not capable of recognizing failed decryptions due to incorrect keys. This mirrors the behavior of using, for example, AES-CBC without an HMAC in real life. AEAD_DEC is capable of failing on decryption and recognizing failed decryptions, which is why it supports checks (“?”)

This is what appears to be forcing you to use HMACs, for which have a checked ASSERT statement right before the DEC statement. However, it’s possible for the active attacker replace the HMAC (thereby allowing ASSERT to pass) without replacing the ciphertext, no? Therefore, the ASSERT would pass, but the false ciphertext would still be decrypted afterwards.

Please let me know if I’m misinterpreting something.

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

> On 15 Nov 2019, at 5:10 PM, jq-rs at mles.io wrote:
> 
> 
> Hello,
> 
> Still wondering this, are the ENC(nil, nil) and MAC(nil, nil) bugs or do I have something to worry about in the protocol?
> 
> E.g.
> 
> "Result! cipher_msg_bob_name, sent by Attacker and not by Bob and resolving to ENC(nil, nil), is successfully used in primitive DEC(HASH(HASH(key_string)), ENC(nil, nil)) in Alice's state (analysis 44, depth 0)"
> 
> Thanks for looking into it,
> -- 
>  jq-rs
> 
> On Fri, 1 Nov 2019, at 8:11 PM, jq-rs at mles.io wrote:
>> 
>> Hello,
>> 
>> I upgraded mles-webworker model to 0.7.5 and seems it has new findings 
>> with nil-parameters. I am afraid I can't quite get them. Any guidance? 
>> Thank you.
>> 
>> Verifpal 0.7.5 (go1.13.3)
>> © 2019 Nadim Kobeissi — https://verifpal.com
>> WARNING: Verifpal is experimental software.
>> 
>> Verifpal! parsing model "mles-websocket.vp"...
>> Verifpal! verification initiated at 17:56:48
>> Analysis! Alice has sent cipher_msg_alice_name to Bob, rendering it 
>> public
>> Analysis! Alice has sent cipher_msg_alice_channel to Bob, rendering it 
>> public
>> Analysis! Alice has sent cipher_msg_alice to Bob, rendering it public
>> Analysis! Alice has sent hmac_cipher_msg_alice to Bob, rendering it 
>> public
>> Analysis! Bob has sent cipher_msg_bob_name to Alice, rendering it 
>> public
>> Analysis! Bob has sent cipher_msg_bob_channel to Alice, rendering it 
>> public
>> Analysis! Bob has sent cipher_msg_bob to Alice, rendering it public
>> Analysis! Bob has sent hmac_cipher_msg_bob to Alice, rendering it 
>> public
>>     Info! attacker is configured as active
>> Deduction! cipher_msg_alice_name resolves to 
>> ENC(HASH(HASH(key_string)), name_alice)
>> Deduction! ENC(HASH(HASH(key_string)), channel) found by attacker by 
>> equivocating with cipher_msg_alice_channel (analysis 0, depth 1)
>> Deduction! cipher_msg_alice resolves to ENC(HASH(key_string), 
>> msg_alice) (analysis 0, depth 2)
>> Deduction! hmac_cipher_msg_alice resolves to 
>> MAC(HASH(HASH(key_string)), ENC(HASH(key_string), msg_alice)) (analysis 
>> 0, depth 3)
>> Deduction! cipher_msg_bob_name resolves to ENC(HASH(HASH(key_string)), 
>> name_bob) (analysis 0, depth 4)
>> Deduction! cipher_msg_bob resolves to ENC(HASH(key_string), msg_bob) 
>> (analysis 0, depth 5)
>> Deduction! hmac_cipher_msg_bob resolves to MAC(HASH(HASH(key_string)), 
>> ENC(HASH(key_string), msg_bob)) (analysis 0, depth 6)
>> Analysis! ASSERT(MAC(HASH(HASH(key_string)), ENC(HASH(key_string), 
>> msg_alice)), MAC(HASH(HASH(key_string)), ENC(HASH(key_string), 
>> msg_alice)))? now conceivable by reconstructing with 
>> MAC(HASH(HASH(key_string)), ENC(HASH(key_string), msg_alice)), 
>> MAC(HASH(HASH(key_string)), ENC(HASH(key_string), msg_alice)) (analysis 
>> 0, depth 7)
>> Analysis! ASSERT(MAC(HASH(HASH(key_string)), ENC(HASH(key_string), 
>> msg_bob)), MAC(HASH(HASH(key_string)), ENC(HASH(key_string), 
>> msg_bob)))? now conceivable by reconstructing with 
>> MAC(HASH(HASH(key_string)), ENC(HASH(key_string), msg_bob)), 
>> MAC(HASH(HASH(key_string)), ENC(HASH(key_string), msg_bob)) (analysis 
>> 0, depth 8)
>> Analysis! MAC(nil, nil) now conceivable by reconstructing with nil, 
>> nil (analysis 9, depth 0)
>> Analysis! ASSERT(MAC(HASH(HASH(key_string)), ENC(HASH(key_string), 
>> msg_alice)), MAC(nil, nil))? now conceivable by reconstructing with 
>> MAC(HASH(HASH(key_string)), ENC(HASH(key_string), msg_alice)), MAC(nil, 
>> nil) (analysis 9, depth 1)
>> Deduction! ENC(nil, nil) found by attacker by reconstructing with nil 
>> (analysis 12, depth 0)
>>   Result! cipher_msg_alice_name, sent by Attacker and not by Alice and 
>> resolving to ENC(nil, nil), is successfully used in primitive 
>> DEC(HASH(HASH(key_string)), ENC(nil, nil)) in Bob's state (analysis 21, 
>> depth 0)
>> Analysis! MAC(nil, nil) now conceivable by reconstructing with nil, 
>> nil (analysis 32, depth 0)
>> Analysis! ASSERT(MAC(HASH(HASH(key_string)), ENC(HASH(key_string), 
>> msg_bob)), MAC(nil, nil))? now conceivable by reconstructing with 
>> MAC(HASH(HASH(key_string)), ENC(HASH(key_string), msg_bob)), MAC(nil, 
>> nil) (analysis 32, depth 1)
>> Deduction! ENC(nil, nil) found by attacker by reconstructing with nil 
>> (analysis 35, depth 0)
>>   Result! cipher_msg_bob_name, sent by Attacker and not by Bob and 
>> resolving to ENC(nil, nil), is successfully used in primitive 
>> DEC(HASH(HASH(key_string)), ENC(nil, nil)) in Alice's state (analysis 
>> 44, depth 0)
>> Stage 2, Analysis 52...
>>   Result! authentication? Alice -> Bob: cipher_msg_alice_name: 
>> cipher_msg_alice_name, sent by Attacker and not by Alice and resolving 
>> to ENC(nil, nil), is successfully used in primitive 
>> DEC(HASH(HASH(key_string)), ENC(nil, nil)) in Bob's state
>>   Result! authentication? Bob -> Alice: cipher_msg_bob_name: 
>> cipher_msg_bob_name, sent by Attacker and not by Bob and resolving to 
>> ENC(nil, nil), is successfully used in primitive 
>> DEC(HASH(HASH(key_string)), ENC(nil, nil)) in Alice's state
>> Verifpal! verification completed at 17:56:48
>> 
>> https://github.com/jq-rs/mles-webworker/blob/master/mles-websocket.vp
>> 
>> -- 
>>  jq-rs at mles.io
> 
> _______________________________________________
> Verifpal mailing list
> Verifpal at lists.symbolic.software
> https://lists.symbolic.software/mailman/listinfo/verifpal