[Verifpal] Feature request: ring signatures

Nadim Kobeissi nadim at symbolic.software
Wed Feb 12 15:50:44 CET 2020


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/20200212/9b8174f3/attachment.htm>


More information about the Verifpal mailing list