[Verifpal] New analysis with nil

jq-rs at mles.io jq-rs at mles.io
Sun Nov 17 16:26:34 CET 2019 

Hello,

Yes, that is a problem. Luckily, it seems that my model is not accurate, so in the real protocol the HMAC is constructed over all parts of the transmitted data instead of the message part only. Verifpal is a great tool to point this out.

Thank you,
-- 
  jq-rs

On Sun, 17 Nov 2019, at 12:13 PM, Nadim Kobeissi wrote:
> No, the HMAC would not be replaced. The HMAC would be kept intact, 
> while the message passed to DEC would be replaced. You are decrypting 
> cipher_msg_alice_name while applying the HMAC on a different value.
> 
> Nadim Kobeissi
> Symbolic Software • https://symbolic.software
> 
> > On 16 Nov 2019, at 4:48 PM, jq-rs at mles.io wrote:
> > 
> > 
> > Hello,
> > 
> > Thank you for the analysis!
> > 
> > HMAC is indeed used to verify both the data integrity and the authenticity of the messages. Nevertheless, I believe the attacker would need to know the correct HMAC key to pass the ASSERT. The HMAC key is not available for the attacker, so even if the HMAC part of the message would be replaced, it should not pass the check.
> > 
> > Let me know if I can provide any further details.
> > 
> > BR,
> > --
> >  jq-rs
> > 
> > On Sat, 16 Nov 2019, at 2:28 PM, Nadim Kobeissi wrote:
> >> 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
> >> 
> >> 
> 
>

More information about the Verifpal mailing list