[Verifpal] Concatenate values

Friedrich Wiemer friedrich.wiemer at rub.de
Sat Feb 29 15:25:11 CET 2020

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.


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:
>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
>> 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
>> _______________________________________________
>> Verifpal mailing list
>> Verifpal at lists.symbolic.software
>> https://lists.symbolic.software/mailman/listinfo/verifpal
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20200229/8905198d/attachment.htm>

More information about the Verifpal mailing list