[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.

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
>>
>> _______________________________________________
>> 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