[Verifpal] New analysis with nil

[jq-rs at mles.io]

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