[Verifpal] ProVerif translation & split
nadim at symbolic.software
Sun Jun 7 10:33:09 CEST 2020
Thanks for reporting this! Issue should be fixed now in the master branch, and the fix will be part of Verifpal 0.14.1.
Symbolic Software • https://symbolic.software
> On 2 Jun 2020, at 8:02 PM, Friedrich Wiemer via Verifpal <verifpal at lists.symbolic.software> wrote:
> Signed PGP part
> I tried the proverif translation and it seems to have a problem when the
> verifpal model uses the concat/split functions. The attached model
> throws the following error when the translated proverif model is feeded
> to it:
>> % verifpal translate pv concat.vp > concat.pv && proverif concat.pv
>> File "concat.pv", line 127, characters 63-69:
>> Warning: identifier Alice_m rebound.
>> File "concat.pv", line 146, characters 63-71:
>> Warning: identifier Bob_m_dec rebound.
>> File "concat.pv", line 147, characters 53-58:
>> Error: SPLIT1 not defined.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 228 bytes
Desc: Message signed with OpenPGP
More information about the Verifpal