[Verifpal] Feature request: ring signatures

Nadim Kobeissi nadim at symbolic.software
Sun Feb 16 17:13:15 CET 2020


A quick update: in Verifpal 0.11.4, the following query in
ringsign_substitute.vp, which used to pass in older versions, now fails
(the model itself was not changed in any way):

authentication? Bob -> Damian: m

Instead of the query passing, we get this result:
Result • authentication? Bob -> Damian: m: When the following values are
controlled by Attacker:
           m → m (originally m)
           sb → RINGSIGN(a, G^b, G^c, m) (originally RINGSIGN(b, ga, gc, m))
           m (m), sent by Attacker and not by Bob, is successfully used in
RINGSIGNVERIF(G^a, G^b, G^c, m, RINGSIGN(a, G^b, G^c, m))? within Damian's
state.

I think this is another step in obtaining what Sebastian was trying to
express in his model, and I think this is a more appropriate query result.

Nadim Kobeissi
Symbolic Software • https://symbolic.software
Sent from office


On Wed, Feb 12, 2020 at 3:50 PM Nadim Kobeissi <nadim at symbolic.software>
wrote:

> Dear Sebastian,
>
> In your Gist model, two of the queries that you illustrate are strange to
> me. You seem to be testing for the authentication properties of Alice, Bob,
> and Carol sending `m`. And yet, Alice and Carol both cannot possibly
> communicate m at any point since they can never possess knowledge of `m`
> according to what you've described in your model. That is what Verifpal is
> complaining about.
>
> The only valid query, `authentication? Bob -> Damian: m`, as you note,
> passes, with Verifpal finding no contradictions. You note that this result
> is not sufficiently precise, and that a more precise result would
> be `authentication? {Alice, Bob, Carol} -> Damian: m`. I completely agree.
> And yet, specifically in your model, the fact that this query passes is
> fine, because Alice and Carol indeed never know `m`, so they cannot ever
> send it to Damian despite owning signature keys within the same ring
> signature key domain.
>
> Let's try a different model, in which Alice and Carol actually know `m`
> and generate their own signatures, `sa` and `sc`, which they also send to
> Damian:
>
> https://source.symbolic.software/verifpal/verifpal/src/branch/master/examples/test/ringsign_substitute.vp
>
>
> Here, we obtain the following results (in Verifpal 0.11.2 -- make sure to
> update, some unrelated issues are fixed that make this result possible):
>
> ```
>    Result • authentication? Alice -> Damian: m:
>            m (m), sent by Bob and not by Alice, is successfully used in
> RINGSIGNVERIF(G^a, G^b, G^c, m, RINGSIGN(b, G^a, G^c, m))? within Damian's
> state.
>
>    Result • authentication? Carol -> Damian: m:
>            m (m), sent by Bob and not by Carol, is successfully used in
> RINGSIGNVERIF(G^a, G^b, G^c, m, RINGSIGN(b, G^a, G^c, m))? within Damian's
> state.
>
>    Result • authentication? Bob -> Damian: sb[
>                 precondition[Bob -> Damian: m]
>         ]: When the following values are controlled by Attacker:
>            sb → RINGSIGN(c, G^a, G^b, m) (originally RINGSIGN(b, G^a, G^c,
> m))
>            sb (RINGSIGN(c, G^a, G^b, m)), sent by Attacker and not by Bob,
> is successfully used in RINGSIGNVERIF(G^a, G^b, G^c, m, RINGSIGN(c, G^a,
> G^b, m))? within Damian's state.
>            Furthermore, the following options are contradicted:
>              - Bob sends m to Damian despite the query being contradicted.
> ```
>
> These results, especially with the usage of a precondition, get closer to
> illustrating what I think you were targeting. I agree however that we can
> be more explicit in expressing what you're trying to say, and look forward
> to further suggestions. For now however, updating to Verifpal 0.11.2 and
> trying the above queries should help with progressing.
>
> Nadim Kobeissi
> Symbolic Software • https://symbolic.software
> Sent from office
>
>
> On Wed, Feb 12, 2020 at 6:24 AM Sebastian Verschoor <
> sebastian.verschoor at gmail.com> wrote:
>
>> Hi Nadim,
>>
>> Unfortunately I am not very proficient in go, so I couldn't say to much
>> about the code directly.
>>
>> However, I can understand the tests you wrote. To be honest, I am a bit
>> surprised that the first test succeeds. I would have expected
>> `authentication? Bob -> Damian: m` to fail, as a ring-signature does not
>> provide such a guarantee. Instead, it guarantees `authentication? {Alice,
>> Bob, Carol} -> Damian: m`. I don't think Verifpal currently has the syntax
>> to express this. I played a bit with it here:
>> https://gist.github.com/sebastianv89/bbab7402dcd047923254aab392c7f675
>> but that code gives an error.
>>
>> The second test fails for the right reason, so that is a good indication.
>>
>> Best,
>> Sebastian
>>
>> On Fri, 7 Feb 2020 at 14:47, Nadim Kobeissi <nadim at symbolic.software>
>> wrote:
>>
>>> Sebastian,
>>>
>>> It would be nice to get your feedback on this:
>>>
>>> https://source.symbolic.software/verifpal/verifpal/commit/fbc4d7372c0fe7df484d7331f045ff5710a63d37
>>>
>>> https://source.symbolic.software/verifpal/verifpal/commit/29c0f2121c4e9bb0ce377e0571defc46c551b275
>>>
>>> You can try it yourself by compiling Verifpal straight from the master
>>> branch.
>>>
>>> Looking forward to hearing your thoughts,
>>>
>>> Nadim Kobeissi
>>> Symbolic Software • https://symbolic.software
>>>
>>> > On 6 Feb 2020, at 11:06 PM, Nadim Kobeissi <nadim at symbolic.software>
>>> wrote:
>>> >
>>> > Hi Sebastian,
>>> >
>>> > I see what you mean; I’ll endeavor to have this supported in Verifpal
>>> soon. If you have other suggestions, please communicate them!
>>> >
>>> > Thanks,
>>> >
>>> > Nadim Kobeissi
>>> > Symbolic Software • https://symbolic.software
>>> >
>>> >> On 6 Feb 2020, at 4:26 PM, Sebastian Verschoor <
>>> sebastian.verschoor at gmail.com> wrote:
>>> >>
>>> >>
>>> >>
>>> >> On Thu, 6 Feb 2020 at 10:24, Sebastian R. Verschoor <
>>> srverschoor at uwaterloo.ca> wrote:
>>> >> Hi Nadim,
>>> >>
>>> >> The signature function has a small typo I think (ga should be gb)
>>> >> `s = RINGSIGN(a, m, G^a, gb, gc)`
>>> >> and for the verification the argument `ga` is repeated, so instead:
>>> >> `_ = RINGSIGNVERIF(m, s, ga, G^b, gc)?`
>>> >>
>>> >> However, one important detail is that the verification function does
>>> not leak which principal actually created the signature, for example
>>> through the argument order. In other words, the following verifications
>>> should all succeed.
>>> >> `_ = RINGSIGNVERIF(m, s, ga, gc, G^b)?`
>>> >> `_ = RINGSIGNVERIF(m, s, G^b, ga, gc)?`
>>> >> `_ = RINGSIGNVERIF(m, s, G^b, gc, ga)?`
>>> >> `_ = RINGSIGNVERIF(m, s, gc, ga, G^b)?`
>>> >> `_ = RINGSIGNVERIF(m, s, gc, G^b, ga)?`
>>> >>
>>> >> Of course this means there are n factorial verification functions for
>>> a signature using n keys. Maybe a more intuitive implementation would be to
>>> instead implement this over the set of public keys (because in sets the
>>> order does not matter):
>>> >> `s = RINGSIGN(a, m, {G^a, gb, gc})`
>>> >> `_ = RINGSIGNVERIF(m, s, {G^b, ga, gc})`
>>> >>
>>> >> Thanks!
>>> >> Sebastian
>>> >>
>>> >>
>>> >> On Thu, 6 Feb 2020 at 09:46, Nadim Kobeissi <nadim at symbolic.software>
>>> wrote:
>>> >> Dear Sebastian,
>>> >>
>>> >> Ring signatures sounds like a great primitive to add to Verifpal. I
>>> propose the following interface:
>>> >>
>>> >> ```
>>> >> principal Alice[
>>> >>        knows private a
>>> >>        knows private m
>>> >>        ga = G^a
>>> >>        // Alice has previously received G^b, G^c
>>> >>        s = RINGSIGN(a, m, G^a, ga, gc)
>>> >> ]
>>> >>
>>> >> Alice -> Bob: m, s, ga
>>> >>
>>> >> principal Bob[
>>> >>        _ = RINGSIGNVERIF(ga, m, s, ga, G^b, gc)?
>>> >> ]
>>> >> ```
>>> >>
>>> >> Would this interface work for your use case?
>>> >>
>>> >> Thank you,
>>> >>
>>> >> Nadim Kobeissi
>>> >> Symbolic Software • https://symbolic.software
>>> >>
>>> >>> On 5 Feb 2020, at 10:01 PM, Sebastian Reynaldo Verschoor via
>>> Verifpal <verifpal at lists.symbolic.software> wrote:
>>> >>>
>>> >>> Hi,
>>> >>>
>>> >>> Not sure if this is the way to do it, but I'd like to request a new
>>> crypto primitive for Verifpal, namely ring signatures.
>>> >>> The reason is that I'd be interested in modelling OTRv4, where ring
>>> signatures are used for deniability. (In that context, I would only need
>>> unlinkable, untraceable signatures over three public keys, if that makes
>>> the request easier?)
>>> >>> As a possible alternative, I was wondering if you are planning the
>>> option for the user to construct their own primitives in some future
>>> release?
>>> >>>
>>> >>> Thanks,
>>> >>> Sebastian
>>> >>>
>>> >>>
>>> >>> _______________________________________________
>>> >>> Verifpal mailing list
>>> >>> Verifpal at lists.symbolic.software
>>> >>> https://lists.symbolic.software/mailman/listinfo/verifpal
>>> >>
>>> >
>>>
>>>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20200216/de998250/attachment.htm>


More information about the Verifpal mailing list