[Verifpal] Sample analysis of a websocket protocol

[jq-rs at mles.io]

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