[Verifpal] ProVerif translation & split

Friedrich Wiemer friedrich.wiemer at rub.de
Tue Jun 2 20:02:00 CEST 2020


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

-------------- next part --------------
attacker[active]

principal Alice[
    knows private k_ab
]
principal Bob[
    knows private k_ab
]

principal Alice[
    generates Na
    generates m1

    m = CONCAT(Na, m1)
    e_m = AEAD_ENC(k_ab, m, nil)
]
Alice -> Bob: e_m

principal Bob[
    m_dec = AEAD_DEC(k_ab, e_m, nil)?
    Na_dec, m1_dec = SPLIT(m_dec)
]

queries[
    confidentiality? m
]
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 488 bytes
Desc: not available
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20200602/b49964be/attachment.sig>


More information about the Verifpal mailing list