Verifpal 0.26.1 - https://verifpal.com
  Warning • Verifpal is Beta software. 
 Verifpal • Parsing model '1v1_simple.vp'...
 Verifpal • Verification initiated for '1v1_simple.vp' at 09:03:56 AM.
     Info • Attacker is configured as active.
     Info • Running at phase 0.
 Analysis • Constructed skeleton HKDF(nil, nil, nil) based on HKDF(salt, s, info).
 Analysis • Constructed skeleton HKDF(nil, nil, nil) based on HKDF(salt, s, info).
 Analysis • Constructed skeleton AEAD_DEC(HKDF(nil, nil, nil), AEAD_ENC(HKDF(nil, nil, nil), nil, HKDF(nil, nil, nil)), HKDF(nil, nil, nil)) based on AEAD_DEC(HKDF(salt, s, info), AEAD_ENC(HKDF(salt, s, info), ma0, HKDF(salt, s, info)), HKDF(salt, s, info)).
 Stage 0, Analysis 1...
 Stage 0, Analysis 2...
 Analysis • Initializing Stage 1 mutation map for Alice...
   Result • authentication? Bob -> Alice: eb0 — When:
            ea0 → AEAD_ENC(HKDF(salt, s, info), ma0, HKDF(salt, s, info)) ← obtained by Attacker
            db0 → AEAD_DEC(HKDF(salt, s, info), AEAD_ENC(HKDF(salt, s, info), ma0, HKDF(salt, s, info)), HKDF(salt, s, info))
            eb0 → AEAD_ENC(HKDF(salt, s, info), mb0, HKDF(salt, s, info))
            da0 → AEAD_DEC(HKDF(salt, s, info), AEAD_ENC(HKDF(salt, s, info), mb0, HKDF(salt, s, info)), HKDF(salt, s, info))

            In another session:
            ea0 → AEAD_ENC(HKDF(salt, s, info), ma0, HKDF(salt, s, info))
            db0 → ma0
            eb0 → AEAD_ENC(HKDF(salt, s, info), ma0, HKDF(salt, s, info)) ← mutated by Attacker (originally AEAD_ENC(kb, mb0, ib))
            da0 → ma0
            eb0 (AEAD_ENC(HKDF(salt, s, info), ma0, HKDF(salt, s, info))), sent by Attacker and not by Bob, is successfully used in AEAD_DEC(HKDF(salt, s, info), AEAD_ENC(HKDF(salt, s, info), ma0, HKDF(salt, s, info)), HKDF(salt, s, info)) within Alice's state.
 (Analysis 2)
Deduction • Output of AEAD_ENC(HKDF(nil, nil, nil), nil, HKDF(nil, nil, nil)) obtained by decomposing AEAD_DEC(HKDF(nil, nil, nil), AEAD_ENC(HKDF(nil, nil, nil), nil, HKDF(nil, nil, nil)), HKDF(nil, nil, nil)) with HKDF(nil, nil, nil). (Analysis 2)
 Stage 1, Analysis 3...
 Analysis • Initializing Stage 1 mutation map for Bob...
   Result • authentication? Alice -> Bob: ea0 — When:
            ea0 → AEAD_ENC(HKDF(salt, s, info), ma0, HKDF(salt, s, info))
            db0 → AEAD_DEC(HKDF(salt, s, info), AEAD_ENC(HKDF(salt, s, info), ma0, HKDF(salt, s, info)), HKDF(salt, s, info))
            eb0 → AEAD_ENC(HKDF(salt, s, info), mb0, HKDF(salt, s, info)) ← obtained by Attacker
            da0 → AEAD_DEC(HKDF(salt, s, info), AEAD_ENC(HKDF(salt, s, info), mb0, HKDF(salt, s, info)), HKDF(salt, s, info))

            In another session:
            ea0 → AEAD_ENC(HKDF(salt, s, info), mb0, HKDF(salt, s, info)) ← mutated by Attacker (originally AEAD_ENC(ka, ma0, ia))
            db0 → mb0
            eb0 → AEAD_ENC(HKDF(salt, s, info), mb0, HKDF(salt, s, info))
            da0 → mb0
            ea0 (AEAD_ENC(HKDF(salt, s, info), mb0, HKDF(salt, s, info))), sent by Attacker and not by Alice, is successfully used in AEAD_DEC(HKDF(salt, s, info), AEAD_ENC(HKDF(salt, s, info), mb0, HKDF(salt, s, info)), HKDF(salt, s, info)) within Bob's state.
 (Analysis 3)
 Stage 1, Analysis 4...
 Analysis • Initializing Stage 3 mutation map for Alice...
 Analysis • Initializing Stage 2 mutation map for Alice...
 Stage 2-3, Analysis 5...
 Stage 2-3, Analysis 6...
 Stage 2-3, Analysis 7...
 Analysis • Initializing Stage 2 mutation map for Bob...
 Stage 2-3, Analysis 8...
Deduction • Output of AEAD_ENC(HKDF(nil, nil, nil), nil, HKDF(nil, nil, nil)) obtained by reconstructing with HKDF(nil, nil, nil), nil, HKDF(nil, nil, nil). (Analysis 8)
 Stage 2-3, Analysis 9...
 Stage 2-3, Analysis 10...
Deduction • Output of AEAD_ENC(HKDF(nil, nil, nil), nil, HKDF(nil, nil, nil)) obtained by reconstructing with HKDF(nil, nil, nil), nil, HKDF(nil, nil, nil). (Analysis 10)
 Stage 2-3, Analysis 11...
 Stage 2-3, Analysis 12...
Deduction • Output of AEAD_ENC(HKDF(nil, nil, nil), nil, HKDF(nil, nil, nil)) obtained by reconstructing with HKDF(nil, nil, nil), nil, HKDF(nil, nil, nil). (Analysis 11)
 Stage 2-3, Analysis 13...
 Stage 2-3, Analysis 14...
 Analysis • Initializing Stage 3 mutation map for Bob...
 Stage 2-3, Analysis 15...
 Stage 2-3, Analysis 16...
 Stage 2-3, Analysis 17...
 Stage 2-3, Analysis 18...
 Stage 2-3, Analysis 19...
 Stage 2-3, Analysis 20...
 Analysis • Initializing Stage 5 mutation map for Alice...
 Analysis • Initializing Stage 4 mutation map for Alice...
 Stage 4-5, Analysis 21...
 Stage 4-5, Analysis 22...
 Stage 4-5, Analysis 23...
 Stage 4-5, Analysis 24...
 Stage 4-5, Analysis 25...
 Stage 4-5, Analysis 26...
 Stage 4-5, Analysis 27...
 Stage 4-5, Analysis 28...
 Stage 4-5, Analysis 29...
 Stage 4-5, Analysis 30...
 Stage 4-5, Analysis 31...
 Stage 4-5, Analysis 32...
 Stage 4-5, Analysis 33...
 Stage 4-5, Analysis 34...
 Stage 4-5, Analysis 35...
 Stage 4-5, Analysis 36...
 Analysis • Initializing Stage 4 mutation map for Bob...
 Stage 4-5, Analysis 37...
 Stage 4-5, Analysis 38...
 Analysis • Initializing Stage 5 mutation map for Bob...
 Stage 4-5, Analysis 39...
 Stage 4-5, Analysis 40...
 Stage 4-5, Analysis 41...
 Stage 4-5, Analysis 42...
 Stage 4-5, Analysis 43...
 Stage 4-5, Analysis 44...
 Stage 4-5, Analysis 45...
 Stage 4-5, Analysis 46...
 Stage 4-5, Analysis 47...
 Stage 4-5, Analysis 48...
 Stage 4-5, Analysis 50...
 Stage 4-5, Analysis 49...
 Stage 4-5, Analysis 51...
 Stage 4-5, Analysis 52...
 Stage 4-5, Analysis 53...
 Stage 4-5, Analysis 55...
 Stage 4-5, Analysis 54...
 Stage 4-5, Analysis 56...
 Analysis • Initializing Stage 6 mutation map for Alice...
 Stage 6, Analysis 57...
 Stage 6, Analysis 58...
 Stage 6, Analysis 59...
 Stage 6, Analysis 60...
 Stage 6, Analysis 61...
 Stage 6, Analysis 62...
 Stage 6, Analysis 63...
 Stage 6, Analysis 64...
 Stage 6, Analysis 65...
 Analysis • Initializing Stage 6 mutation map for Bob...
 Stage 6, Analysis 66...
 Stage 6, Analysis 67...
 Stage 6, Analysis 68...
 Stage 6, Analysis 69...
 Stage 6, Analysis 70...
 Stage 6, Analysis 71...
 Stage 6, Analysis 72...
 Stage 6, Analysis 73...
 Stage 6, Analysis 74...


 Verifpal • Verification completed for '1v1_simple.vp' at 09:03:56 AM.
 Verifpal • Summary of failed queries will follow.

   Result • authentication? Alice -> Bob: ea0 — When:
            ea0 → AEAD_ENC(HKDF(salt, s, info), ma0, HKDF(salt, s, info))
            db0 → AEAD_DEC(HKDF(salt, s, info), AEAD_ENC(HKDF(salt, s, info), ma0, HKDF(salt, s, info)), HKDF(salt, s, info))
            eb0 → AEAD_ENC(HKDF(salt, s, info), mb0, HKDF(salt, s, info)) ← obtained by Attacker
            da0 → AEAD_DEC(HKDF(salt, s, info), AEAD_ENC(HKDF(salt, s, info), mb0, HKDF(salt, s, info)), HKDF(salt, s, info))

            In another session:
            ea0 → AEAD_ENC(HKDF(salt, s, info), mb0, HKDF(salt, s, info)) ← mutated by Attacker (originally AEAD_ENC(ka, ma0, ia))
            db0 → mb0
            eb0 → AEAD_ENC(HKDF(salt, s, info), mb0, HKDF(salt, s, info))
            da0 → mb0
            ea0 (AEAD_ENC(HKDF(salt, s, info), mb0, HKDF(salt, s, info))), sent by Attacker and not by Alice, is successfully used in AEAD_DEC(HKDF(salt, s, info), AEAD_ENC(HKDF(salt, s, info), mb0, HKDF(salt, s, info)), HKDF(salt, s, info)) within Bob's state.

   Result • authentication? Bob -> Alice: eb0 — When:
            ea0 → AEAD_ENC(HKDF(salt, s, info), ma0, HKDF(salt, s, info)) ← obtained by Attacker
            db0 → AEAD_DEC(HKDF(salt, s, info), AEAD_ENC(HKDF(salt, s, info), ma0, HKDF(salt, s, info)), HKDF(salt, s, info))
            eb0 → AEAD_ENC(HKDF(salt, s, info), mb0, HKDF(salt, s, info))
            da0 → AEAD_DEC(HKDF(salt, s, info), AEAD_ENC(HKDF(salt, s, info), mb0, HKDF(salt, s, info)), HKDF(salt, s, info))

            In another session:
            ea0 → AEAD_ENC(HKDF(salt, s, info), ma0, HKDF(salt, s, info))
            db0 → ma0
            eb0 → AEAD_ENC(HKDF(salt, s, info), ma0, HKDF(salt, s, info)) ← mutated by Attacker (originally AEAD_ENC(kb, mb0, ib))
            da0 → ma0
            eb0 (AEAD_ENC(HKDF(salt, s, info), ma0, HKDF(salt, s, info))), sent by Attacker and not by Bob, is successfully used in AEAD_DEC(HKDF(salt, s, info), AEAD_ENC(HKDF(salt, s, info), ma0, HKDF(salt, s, info)), HKDF(salt, s, info)) within Alice's state.

 Verifpal • Thank you for using Verifpal.