[Verifpal] New analysis with nil

[jq-rs at mles.io]

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