[Verifpal] Sample analysis of a websocket protocol

[Nadim Kobeissi]

Dear jq-rs,

I am so pleased to see that you’ve found a usage for Verifpal!

Your protocol is relatively simple and does not rely on public-key cryptography, but I still think Verifpal can be useful since, as you write your model, you can:

1. Reason better about your protocol yourself,
2. Communicate its specification to others,
3. Prototype the potential effects of removing certain keys, etc.
4. Model and prototype for future additions to the protocol.

It’s really great to see people finding Verifpal useful already.

“Deduction” doesn’t mean anything dangerous :-) it’s just Verifpal informing you that the attacker has realized that it can learn new values.

Keep us updated on your progress, and thank you!

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

> On Sep 3, 2019, at 9:31 PM, jq-rs at mles.io wrote:
> 
> 
> Hello,
> 
> Thanks for this awesome (still experimental) software! I really value the premises it has, there is a real need for it.
> 
> I gave a test run for MlesTalk WebWorker protocol which is a simple hash + cbc based protocol on websocket which uses pre-shared key. The results are pretty expected with the description file at https://github.com/jq-rs/mles-webworker/blob/master/mles-websocket.vp
> 
> Please see analysis below. I am a bit uncertain what deduction means? Maybe nothing to worry about as results are solid.
> 
> I can easily see future improvements of the protocol verified with Verifpal, if such improvements emerge. And my mind is already thinking about verifying user changes and forward secrecy (even though I planned to keep it simple). 
> 
> I am happy to run test runs in the future, if it helps in any way.
> 
> Verifpal 0.3 (https://verifpal.com)
> c 2019 Symbolic Software
> WARNING: Verifpal is experimental software.
> 
> Verifpal! parsing model...
> Verifpal! verification initiated at 21:56:05
> 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 attacker
> Deduction! cipher_msg_alice_name resolves to ENC(ecb_key_alice, name_alice)
> Deduction! ENC(ecb_key_bob, channel) found by attacker by equivocating with cipher_msg_alice_channel (depth 1)
> Deduction! ENC(ecb_key_alice, channel) found by attacker by equivocating with cipher_msg_alice_channel (depth 1)
> Deduction! cipher_msg_alice resolves to ENC(cbc_key_alice, msg_alice) (depth 2)
> Deduction! hmac_cipher_msg_alice resolves to HMAC(ecb_key_alice, cipher_msg_alice) (depth 3)
> Deduction! HMAC(ecb_key_bob, cipher_msg_alice) found by attacker by equivocating with hmac_cipher_msg_alice (depth 4)
> Deduction! cipher_msg_bob_name resolves to ENC(ecb_key_bob, name_bob) (depth 5)
> Deduction! cipher_msg_bob resolves to ENC(cbc_key_bob, msg_bob) (depth 6)
> Deduction! hmac_cipher_msg_bob resolves to HMAC(ecb_key_bob, cipher_msg_bob) (depth 7)
> Deduction! HMAC(ecb_key_alice, cipher_msg_bob) found by attacker by equivocating with hmac_cipher_msg_bob (depth 8)
>     Info! phase 1a active attacker complete
> Verifpal! verification completed at 21:56:05
> REMINDER: Verifpal is experimental software and may miss attacks.
> 
> Cheers,
> -- 
>  jq-rs
> 
> _______________________________________________
> Verifpal mailing list
> Verifpal at lists.symbolic.software
> https://lists.symbolic.software/mailman/listinfo/verifpal