[Verifpal] Concatenate values

Nadim Kobeissi nadim at symbolic.software
Sat Feb 29 16:24:42 CET 2020


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
>>> 
>>> _______________________________________________
>>> 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/be4efacc/attachment.htm>


More information about the Verifpal mailing list