[Verifpal] Concatenate values

Friedrich Wiemer friedrich.wiemer at rub.de
Sat Feb 29 20:49:38 CET 2020


Ah, good to know. Seems that my subscription to the mailinglist did not
worked out, mhmm.

Anyway, I have checked the implementation, but it seems that the
concat/split combination does not survive an encryption/decryption
operation. The attached model gives following error:

> % verifpal verify concat.vp
> Verifpal 0.11.6 - https://verifpal.com
>   Warning • Verifpal is experimental software.
>  Verifpal • Parsing model 'concat.vp'...
>  Verifpal • Verification initiated for 'concat.vp' at 08:43:54 PM.
>      Info • Attacker is configured as active.
>      Info • Running at phase 0.
>  Analysis • Constructed skeleton CONCAT(nil, nil). (Analysis 3)
> Deduction • AEAD_ENC(nil, CONCAT(nil, nil), nil) obtained by reconstructing with nil, CONCAT(nil, nil), nil. (Analysis 3)
>  Verifpal! Error: SPLIT must have CONCAT as input but instead has AEAD_DEC(k_ab, AEAD_ENC(nil, CONCAT(nil, nil), nil), nil)?.

Best,
Friedrich

On Sat, Feb 29, 2020 at 04:24:42PM +0100, Nadim Kobeissi wrote:
> 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
> 
-------------- 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/20200229/529080a9/attachment-0001.sig>


More information about the Verifpal mailing list