Split a derived value

[mohit jangid]

Hi All,

I want to split an encrypted value V into two parts, in such a way that the V can not be derived from either of two parts. However, given the two parts, one should be able to compose V back. The value V can not begin with a paired term, it has to split only after one term is constructed from an encryption operation.  

This may sound like a computation model requirement; However, I am wondering if there is some way to model it in Tamarin.

Thank you 

    

[Jannik Dreier]

Dear Mohit,

I am not sure whether I understand all your requirements, but you could
define functions split1/1, split2/1 and merge/2 with the equation

merge(split1(v),split2(v)) = v

This way a value v can be decomposed into two parts, and using the merge
function these parts can be recomposed to obtain v. However, there is no
way to directly obtain v from either split1(v) or split2(v).

Best regards,
Jannik

> --
> You received this message because you are subscribed to the Google
> Groups "tamarin-prover" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to tamarin-prove...@googlegroups.com
> <mailto:tamarin-prove...@googlegroups.com>.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/tamarin-prover/505db32e-ae70-4ab0-9988-0e7cb6b2c6ecn%40googlegroups.com
> <https://groups.google.com/d/msgid/tamarin-prover/505db32e-ae70-4ab0-9988-0e7cb6b2c6ecn%40googlegroups.com?utm_medium=email&utm_source=footer>.

--
Jannik Dreier
Maître de Conférences | Associate Professor
Université de Lorraine | TELECOM Nancy | LORIA
rese...@jannikdreier.net | +33 3 54 95 84 46

[Cas Cremers]

Hi,

Jannik's version looks good, but the question is also: what real-world mechanism are you trying to model?

Let's say you have a bitstring X of length L. If you were to use "split X in the middle to two bitstrings, each of length L/2" then you of course get different security guarantees in practice than when you split using "generate fresh R (of length L); 'split' X into (R) and (R xor X)".

Best,

Cas

To unsubscribe from this group and stop receiving emails from it, send an email to tamarin-prove...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tamarin-prover/4b6759ab-8f25-3dff-4912-c1901634dff9%40jannikdreier.net.

[mohit jangid]

Thank you, Dr. Jannik and  Dr. Cas for the response. Good point about the different security guarantees based on split methods!
For my case, it's bitstring split. So, I assume that using private functions be more suitable than the xor trick. Please let me know if I am wrong.          

[Jannik Dreier]

Let me make two remarks here:

1) In my suggestion all functions are public (no need for private
functions!).

2) If you cut your bitstring in - let's say - half, then my suggested
modelling might not be completely adequate. In particular, in my
suggestion both split values do not leak any information about v, but if
you simply cut a bitstring in half, both halves do leak a lot of
information about the initial value. Depending on what you want to model
and analyze, this might be a problem. (In this sense my modelling is
more accurate for the second solution Cas mentioned, even thought it
uses xor.)

Best,
Jannik

> <https://groups.google.com/d/msgid/tamarin-prover/505db32e-ae70-4ab0-9988-0e7cb6b2c6ecn%40googlegroups.com?utm_medium=email&utm_source=footer

> <https://groups.google.com/d/msgid/tamarin-prover/505db32e-ae70-4ab0-9988-0e7cb6b2c6ecn%40googlegroups.com?utm_medium=email&utm_source=footer>>.
>
> --
> Jannik Dreier
> Maître de Conférences     | Associate Professor
> Université de Lorraine    | TELECOM Nancy | LORIA
> rese...@jannikdreier.net | +33 3 54 95 84 46

> <tel:+33%203%2054%2095%2084%2046>

>
> --
> You received this message because you are subscribed to the
> Google Groups "tamarin-prover" group.
>
> To unsubscribe from this group and stop receiving emails from
> it, send an email to tamarin-prove...@googlegroups.com.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/tamarin-prover/4b6759ab-8f25-3dff-4912-c1901634dff9%40jannikdreier.net

> <https://groups.google.com/d/msgid/tamarin-prover/4b6759ab-8f25-3dff-4912-c1901634dff9%40jannikdreier.net>.

>
> --
> You received this message because you are subscribed to the Google
> Groups "tamarin-prover" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to tamarin-prove...@googlegroups.com
> <mailto:tamarin-prove...@googlegroups.com>.
> To view this discussion on the web visit

> https://groups.google.com/d/msgid/tamarin-prover/727ebaf7-8ae1-42c2-842f-e404cf5c8979n%40googlegroups.com
> <https://groups.google.com/d/msgid/tamarin-prover/727ebaf7-8ae1-42c2-842f-e404cf5c8979n%40googlegroups.com?utm_medium=email&utm_source=footer>.

[mohit jangid]

That is very helpful. Thank you. 

[Frag Dein Pferd]

Hi,

can you please elaborate how

"split X in the middle to two bitstrings, each of length L/2"

is modelled in Tamarin, given that Jannik's remark about both halfs leaking information about X holds?

Best, Melissa

[mohit jangid]

Hi Frag,

In Jannik's provided equational theory each split does not reveal any information about X. In my modeling (https://github.com/OSUSecLab/bluetooth-pairing-formal-verification), this was fine because I assumed the adversary cannot exploit partial information (the split value) unless she has all split values.

In order to model the exploitation of a partial information leak, I assume you have to add more equational theories to define what is possible to compose/derive with the partial information. Also, make sure that those equational theories have finite variant properties and that they are convergent. Dr. Cas and Dr. Jannik can provide more information in this regard.

-- 

Mohit Kumar Jangid

Ph.D. Student at Ohio State University