[Verifpal] Random query results?

Nadim Kobeissi nadim at symbolic.software
Wed Jun 24 13:07:22 CEST 2020


Dear Renaud,

Thank you very much for pointing this out. This is a race condition that was somehow missed by Go’s race detector.

It has been fixed here:
https://source.symbolic.software/verifpal/verifpal/-/commit/a6eee297d9b2c3a1c6b4e03ac7ca024ed764e04c

The fix will be available in the next Verifpal update (which I will likely push today).

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

> On 23 Jun 2020, at 6:13 PM, Renaud Lifchitz via Verifpal <verifpal at lists.symbolic.software> wrote:
> 
> 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
> 
> 
> _______________________________________________
> Verifpal mailing list
> Verifpal at lists.symbolic.software
> https://lists.symbolic.software/mailman/listinfo/verifpal



More information about the Verifpal mailing list