[Verifpal] Random query results?

Renaud Lifchitz renaud.lifchitz at gmail.com
Tue Jun 23 18:13:27 CEST 2020


Hello,

I have this simple protocol using a password to protect a symmetric session
key (passive attacker):
-----
attacker[passive]
principal Alice[
    knows password pwd
]
principal Bob[
    knows password pwd
]
principal Alice[
    knows private message
    generates key
    a_k = ENC(pwd, key)
    a_m = ENC(key, message)
]
Alice -> Bob: a_k, a_m
principal Bob[
    b_k = DEC(pwd, a_k)
    b_message = DEC(b_k, a_m)
]
queries[
confidentiality? message
]
-----

First run gives the good result (message NOT confidential):
-----
$ sha256sum ex4.vp ; verifpal verify ex4.vp
1e726381ac93a31a2ab43f321fcfef85c5608bdb9ddbd411474600a07ad1046c  ex4.vp
Verifpal 0.14.1 - https://verifpal.com
  Warning • Verifpal is Beta software.
 Verifpal • Parsing model 'ex4.vp'...
 Verifpal • Verification initiated for 'ex4.vp' at 06:06:39 PM.
     Info • Attacker is configured as passive.
Deduction • pwd obtained as a password unsafely used within ENC(pwd, key).
(Analysis 1)
Deduction • key obtained by decomposing ENC(pwd, key) with pwd. (Analysis 2)
Deduction • message obtained by decomposing ENC(key, message) with key.
(Analysis 3)
   Result • confidentiality? message:
            message (message) is obtained by Attacker.
 (Analysis 3)
   Result • confidentiality? message:
            message (message) is obtained by Attacker.
 Verifpal • Verification completed for 'ex4.vp' at 06:06:39 PM.
 Verifpal • Thank you for using Verifpal.
-----

Without any change to the original model file, another run unfortunately
gives the wrong result (message is confidential):

-----
$ sha256sum ex4.vp ; verifpal verify ex4.vp
1e726381ac93a31a2ab43f321fcfef85c5608bdb9ddbd411474600a07ad1046c  ex4.vp
Verifpal 0.14.1 - https://verifpal.com
  Warning • Verifpal is Beta software.
 Verifpal • Parsing model 'ex4.vp'...
 Verifpal • Verification initiated for 'ex4.vp' at 06:06:41 PM.
     Info • Attacker is configured as passive.
Deduction • pwd obtained as a password unsafely used within ENC(pwd, key).
(Analysis 1)
Deduction • key obtained by decomposing ENC(pwd, key) with pwd. (Analysis 3)
 Verifpal • Verification completed for 'ex4.vp' at 06:06:41 PM.
 Verifpal • Thank you for using Verifpal.
-----


Am I missing something?

Best regards,

Renaud Lifchitz
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20200623/071bd408/attachment.htm>


More information about the Verifpal mailing list