[Verifpal] ProVerif translation & split

Nadim Kobeissi nadim at symbolic.software
Sun Jun 7 10:33:09 CEST 2020


Dear Friedrich,

Thanks for reporting this! Issue should be fixed now in the master branch, and the fix will be part of Verifpal 0.14.1.

Nadim Kobeissi
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
> Hi,
> 
> 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.
> 
> Best
> Friedrich
> 
> <concat.vp>
> 
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: Message signed with OpenPGP
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20200607/c41347ba/attachment.sig>


More information about the Verifpal mailing list