[Verifpal] Concatenate values

Nadim Kobeissi nadim at symbolic.software
Sun Mar 1 15:15:55 CET 2020


Dear Friedrich,

This was being caused by Verifpal being too overbearing with certain
checks. Verifpal 0.11.7, which will be pushed in a few moments, will
resolve this issue. Please update and try again.

Nadim Kobeissi
Symbolic Software • https://symbolic.software
Sent from office


On Sat, Feb 29, 2020 at 8:49 PM Friedrich Wiemer <friedrich.wiemer at rub.de>
wrote:

> Ah, good to know. Seems that my subscription to the mailinglist did not
> worked out, mhmm.
>
> Anyway, I have checked the implementation, but it seems that the
> concat/split combination does not survive an encryption/decryption
> operation. The attached model gives following error:
>
> > % verifpal verify concat.vp
> > Verifpal 0.11.6 - https://verifpal.com
> >   Warning • Verifpal is experimental software.
> >  Verifpal • Parsing model 'concat.vp'...
> >  Verifpal • Verification initiated for 'concat.vp' at 08:43:54 PM.
> >      Info • Attacker is configured as active.
> >      Info • Running at phase 0.
> >  Analysis • Constructed skeleton CONCAT(nil, nil). (Analysis 3)
> > Deduction • AEAD_ENC(nil, CONCAT(nil, nil), nil) obtained by
> reconstructing with nil, CONCAT(nil, nil), nil. (Analysis 3)
> >  Verifpal! Error: SPLIT must have CONCAT as input but instead has
> AEAD_DEC(k_ab, AEAD_ENC(nil, CONCAT(nil, nil), nil), nil)?.
>
> Best,
> Friedrich
>
> On Sat, Feb 29, 2020 at 04:24:42PM +0100, Nadim Kobeissi wrote:
> > You don’t need to compile Verifpal from source, an update was just pushed
> > (0.11.6) on all release platforms that includes these new features.
> >
> > Nadim Kobeissi
> > Symbolic Software • https://symbolic.software
> > Sent from my iPhone
> >
> >
> >     On 29 Feb 2020, at 3:25 PM, Friedrich Wiemer <
> friedrich.wiemer at rub.de>
> >     wrote:
> >
> >
> >     Dear Nadim,
> >
> >     Great, looks perfect! I don't know go but from the verifpal model
> that
> >     looks like what is needed.
> >
> >     Before I can check further, I have to switch to compile verifpal from
> >     source.
> >
> >     Best,
> >     Friedrich
> >
> >
> >     On February 29, 2020 2:20:31 PM GMT+01:00, Nadim Kobeissi
> >     <nadim at symbolic.software> wrote:
> >
> >         Dear Friedrich,
> >
> >         Your wish is my command. Please review the following commit
> notes:
> >         https://source.symbolic.software/verifpal/verifpal/commit/
> >         87eb78885212c8a40d42696a8156bc8b8cfc121b
> >
> >         Nadim Kobeissi
> >         Symbolic Software • https://symbolic.software
> >         Sent from office
> >
> >
> >         On Fri, Feb 28, 2020 at 10:42 PM Friedrich Wiemer via Verifpal
> >         <verifpal at lists.symbolic.software> wrote:
> >
> >             Hi,
> >
> >             on my way to implement a verifpal model for the
> Needham-Schoeder
> >             protocol, I now need to encrypt a message containing of
> several
> >             parts,
> >             i.e. I would like to do something like the following:
> >
> >             > e1 = AEAD_ENC(key, plain1, plain2, plain3, plain4, nil)
> >             > p1, p2, p3, p4 = AEAD_DEC(key, e1, nil)?
> >
> >             Is there a way to achieve this? I would expect that some
> sort of
> >             concatenation/splitting of constants is needed?
> >
> >             Best,
> >             Friedrich
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20200301/8c0ec13f/attachment.htm>


More information about the Verifpal mailing list