[Verifpal] Verifpal 0.4.1 crash

[Renaud Lifchitz]

Hello,

Using Verifpal 0.4.1 with included example protonmail_to_outside.vp leads
to a crash:
(...)
Deduction! AEAD_ENC(ga^b, m2, ga) found by attacker by equivocating with
em2 (analysis 104, depth 1)
panic: runtime error: index out of range

goroutine 1 [running]:
main.sanityResolveInternalValues(0x5052de, 0x8, 0x0, 0x0, 0x0, 0x0, 0x0,
0x0, 0x0, 0x0, ...)
/home/renaud/installations/verifpal/internal/app/verifpal/sanity.go:487
+0x1037
main.verifyAnalysisReconstruct(0x5052de, 0x8, 0x0, 0x0, 0x0, 0x0, 0x0, 0x0,
0x0, 0x0, ...)
/home/renaud/installations/verifpal/internal/app/verifpal/verifyanalysis.go:125
+0x65
main.verifyAnalysis(0xc0000aa040, 0xc0000cd900, 0xc0004a2050, 0x95, 0x0,
0x1)
/home/renaud/installations/verifpal/internal/app/verifpal/verifyanalysis.go:27
+0x21d
main.verifyActive(0xc0000aa040, 0xc0000cbd80, 0x0, 0x0, 0x505326)
/home/renaud/installations/verifpal/internal/app/verifpal/verifyactive.go:26
+0x54f
main.verify(0xc0000aa040, 0xc0000cbd80, 0xc0000aa040, 0xc0000cbd80, 0x1)
/home/renaud/installations/verifpal/internal/app/verifpal/verify.go:23
+0x4e1
main.main()
/home/renaud/installations/verifpal/internal/app/verifpal/main.go:40 +0x2ef

and verifying included signal.vp seems to take a very long time to complete
due to recent changes in the code...

Thank you.

Best regards,

Renaud Lifchitz
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20190905/d86eff4c/attachment.htm>