New primitive: blind signatures.

This commit introduces blind signatures, as requested by Verifpal
user Professor Marko Schuetz-Schmuck from the University of Puerto
Rico.

Two new primitives are introduced: BLIND and UNBLIND. The interface
works as follows:

```
b = BLIND(k, m)
SIGN(a, b)
UNBLIND(k, m, SIGN(a, BLIND(k, m))) = SIGN(a, m)
```

The purpose of blind signatures is to allow a party to sign a message
without having access to its contents. To fulfill this purpose, a sender
"blinds" a message m with "blinding factor" k and sends the resulting
blinded message m.

The signer signs the blinded message m with their private key a.

Then, using UNBLIND and their blinding factor k, the sender can "unblind"
the signature SIGN(a, BLIND(K, m)) and obtain SIGN(a, m).

Therfore, the signer signed the message without knowing it, and the
sender was able to obtain the signature of the signer on the original
message without revealing the message.

Note that an attacker possessing b and k can obtain m.

An example model is included in `examples/blind.vp`.

Further testing of this new primitive is very much appreciated.

The Verifpal User Manual and Verifpal for Visual Studio Code will be
updated momentarily to reflect the new BLIND and UNBLIND primitives.
parent 98229a2d
Pipeline #192 passed with stages
in 38 seconds
// SPDX-FileCopyrightText: © 2019-2020 Nadim Kobeissi <nadim@symbolic.software>
// SPDX-License-Identifier: GPL-3.0-only
attacker[active]
principal Alice[
generates k
knows private m
b = BLIND(k, m)
]
Alice -> Sarah: b
principal Sarah[
knows private s
gs = G^s
blindsig = SIGN(s, b)
]
Sarah -> Alice: blindsig, gs
principal Alice[
unblindedsig = UNBLIND(k, m, blindsig)
_ = SIGNVERIF(gs, m, unblindedsig)?
]
queries[
confidentiality? m
]
...@@ -19,7 +19,7 @@ func possibleToDecomposePrimitive( ...@@ -19,7 +19,7 @@ func possibleToDecomposePrimitive(
} }
for i, g := range prim.Decompose.Given { for i, g := range prim.Decompose.Given {
a := p.Arguments[g] a := p.Arguments[g]
a, valid := prim.Decompose.Filter(a, i) a, valid := prim.Decompose.Filter(p, a, i)
ii := sanityEquivalentValueInValues(a, valAttackerState.Known) ii := sanityEquivalentValueInValues(a, valAttackerState.Known)
if valid && ii >= 0 { if valid && ii >= 0 {
has = append(has, a) has = append(has, a)
...@@ -197,10 +197,7 @@ func possibleToRewrite( ...@@ -197,10 +197,7 @@ func possibleToRewrite(
if !possibleToRewritePrim(p, valPrincipalState) { if !possibleToRewritePrim(p, valPrincipalState) {
return !prim.Check, v return !prim.Check, v
} }
rewrite := Value{Kind: "primitive", Primitive: p} rewrite := prim.Rewrite.To(from.Primitive)
if prim.Rewrite.To > 0 {
rewrite = from.Primitive.Arguments[prim.Rewrite.To]
}
return true, []Value{rewrite} return true, []Value{rewrite}
} }
return !prim.Check, v return !prim.Check, v
...@@ -215,7 +212,7 @@ func possibleToRewritePrim( ...@@ -215,7 +212,7 @@ func possibleToRewritePrim(
valid := false valid := false
for _, mm := range m { for _, mm := range m {
ax := []Value{p.Arguments[a], from.Primitive.Arguments[mm]} ax := []Value{p.Arguments[a], from.Primitive.Arguments[mm]}
ax[0], valid = prim.Rewrite.Filter(ax[0], mm) ax[0], valid = prim.Rewrite.Filter(p, ax[0], mm)
if !valid { if !valid {
continue continue
} }
......
...@@ -138,7 +138,7 @@ var primitiveSpecs = []PrimitiveSpec{ ...@@ -138,7 +138,7 @@ var primitiveSpecs = []PrimitiveSpec{
HasRule: true, HasRule: true,
Given: []int{0}, Given: []int{0},
Reveal: 1, Reveal: 1,
Filter: func(x Value, i int) (Value, bool) { Filter: func(p Primitive, x Value, i int) (Value, bool) {
return x, true return x, true
}, },
}, },
...@@ -164,7 +164,7 @@ var primitiveSpecs = []PrimitiveSpec{ ...@@ -164,7 +164,7 @@ var primitiveSpecs = []PrimitiveSpec{
HasRule: true, HasRule: true,
Given: []int{0}, Given: []int{0},
Reveal: 1, Reveal: 1,
Filter: func(x Value, i int) (Value, bool) { Filter: func(p Primitive, x Value, i int) (Value, bool) {
return x, true return x, true
}, },
}, },
...@@ -175,12 +175,14 @@ var primitiveSpecs = []PrimitiveSpec{ ...@@ -175,12 +175,14 @@ var primitiveSpecs = []PrimitiveSpec{
HasRule: true, HasRule: true,
Name: "AEAD_ENC", Name: "AEAD_ENC",
From: 1, From: 1,
To: 1, To: func(p Primitive) Value {
return p.Arguments[1]
},
Matching: map[int][]int{ Matching: map[int][]int{
0: {0}, 0: {0},
2: {2}, 2: {2},
}, },
Filter: func(x Value, i int) (Value, bool) { Filter: func(p Primitive, x Value, i int) (Value, bool) {
switch i { switch i {
case 0: case 0:
return x, true return x, true
...@@ -206,7 +208,7 @@ var primitiveSpecs = []PrimitiveSpec{ ...@@ -206,7 +208,7 @@ var primitiveSpecs = []PrimitiveSpec{
HasRule: true, HasRule: true,
Given: []int{0}, Given: []int{0},
Reveal: 1, Reveal: 1,
Filter: func(x Value, i int) (Value, bool) { Filter: func(p Primitive, x Value, i int) (Value, bool) {
return x, true return x, true
}, },
}, },
...@@ -232,7 +234,7 @@ var primitiveSpecs = []PrimitiveSpec{ ...@@ -232,7 +234,7 @@ var primitiveSpecs = []PrimitiveSpec{
HasRule: true, HasRule: true,
Given: []int{0}, Given: []int{0},
Reveal: 1, Reveal: 1,
Filter: func(x Value, i int) (Value, bool) { Filter: func(p Primitive, x Value, i int) (Value, bool) {
return x, true return x, true
}, },
}, },
...@@ -243,11 +245,13 @@ var primitiveSpecs = []PrimitiveSpec{ ...@@ -243,11 +245,13 @@ var primitiveSpecs = []PrimitiveSpec{
HasRule: true, HasRule: true,
Name: "ENC", Name: "ENC",
From: 1, From: 1,
To: 1, To: func(p Primitive) Value {
return p.Arguments[1]
},
Matching: map[int][]int{ Matching: map[int][]int{
0: {0}, 0: {0},
}, },
Filter: func(x Value, i int) (Value, bool) { Filter: func(p Primitive, x Value, i int) (Value, bool) {
switch i { switch i {
case 0: case 0:
return x, true return x, true
...@@ -319,12 +323,14 @@ var primitiveSpecs = []PrimitiveSpec{ ...@@ -319,12 +323,14 @@ var primitiveSpecs = []PrimitiveSpec{
HasRule: true, HasRule: true,
Name: "SIGN", Name: "SIGN",
From: 2, From: 2,
To: -1, To: func(p Primitive) Value {
return constantN
},
Matching: map[int][]int{ Matching: map[int][]int{
0: {0}, 0: {0},
1: {1}, 1: {1},
}, },
Filter: func(x Value, i int) (Value, bool) { Filter: func(p Primitive, x Value, i int) (Value, bool) {
switch i { switch i {
case 0: case 0:
switch x.Kind { switch x.Kind {
...@@ -362,7 +368,7 @@ var primitiveSpecs = []PrimitiveSpec{ ...@@ -362,7 +368,7 @@ var primitiveSpecs = []PrimitiveSpec{
HasRule: true, HasRule: true,
Given: []int{0}, Given: []int{0},
Reveal: 1, Reveal: 1,
Filter: func(x Value, i int) (Value, bool) { Filter: func(p Primitive, x Value, i int) (Value, bool) {
switch i { switch i {
case 0: case 0:
switch x.Kind { switch x.Kind {
...@@ -404,7 +410,7 @@ var primitiveSpecs = []PrimitiveSpec{ ...@@ -404,7 +410,7 @@ var primitiveSpecs = []PrimitiveSpec{
HasRule: true, HasRule: true,
Given: []int{0}, Given: []int{0},
Reveal: 1, Reveal: 1,
Filter: func(x Value, i int) (Value, bool) { Filter: func(p Primitive, x Value, i int) (Value, bool) {
return x, true return x, true
}, },
}, },
...@@ -415,11 +421,13 @@ var primitiveSpecs = []PrimitiveSpec{ ...@@ -415,11 +421,13 @@ var primitiveSpecs = []PrimitiveSpec{
HasRule: true, HasRule: true,
Name: "PKE_ENC", Name: "PKE_ENC",
From: 1, From: 1,
To: 1, To: func(p Primitive) Value {
return p.Arguments[1]
},
Matching: map[int][]int{ Matching: map[int][]int{
0: {0}, 0: {0},
}, },
Filter: func(x Value, i int) (Value, bool) { Filter: func(p Primitive, x Value, i int) (Value, bool) {
switch i { switch i {
case 0: case 0:
switch x.Kind { switch x.Kind {
...@@ -460,7 +468,7 @@ var primitiveSpecs = []PrimitiveSpec{ ...@@ -460,7 +468,7 @@ var primitiveSpecs = []PrimitiveSpec{
{1, 2}, {1, 2},
}, },
Reveal: 0, Reveal: 0,
Filter: func(x Value, i int) (Value, bool) { Filter: func(p Primitive, x Value, i int) (Value, bool) {
return x, true return x, true
}, },
}, },
...@@ -500,7 +508,7 @@ var primitiveSpecs = []PrimitiveSpec{ ...@@ -500,7 +508,7 @@ var primitiveSpecs = []PrimitiveSpec{
{2, 1}, {2, 1},
}, },
Reveal: 0, Reveal: 0,
Filter: func(x Value, i int) (Value, bool) { Filter: func(p Primitive, x Value, i int) (Value, bool) {
return x, true return x, true
}, },
}, },
...@@ -544,14 +552,16 @@ var primitiveSpecs = []PrimitiveSpec{ ...@@ -544,14 +552,16 @@ var primitiveSpecs = []PrimitiveSpec{
HasRule: true, HasRule: true,
Name: "RINGSIGN", Name: "RINGSIGN",
From: 4, From: 4,
To: -1, To: func(p Primitive) Value {
return constantN
},
Matching: map[int][]int{ Matching: map[int][]int{
0: {0, 1, 2}, 0: {0, 1, 2},
1: {0, 1, 2}, 1: {0, 1, 2},
2: {0, 1, 2}, 2: {0, 1, 2},
3: {3}, 3: {3},
}, },
Filter: func(x Value, i int) (Value, bool) { Filter: func(p Primitive, x Value, i int) (Value, bool) {
switch i { switch i {
case 0: case 0:
switch x.Kind { switch x.Kind {
...@@ -587,6 +597,90 @@ var primitiveSpecs = []PrimitiveSpec{ ...@@ -587,6 +597,90 @@ var primitiveSpecs = []PrimitiveSpec{
Explosive: false, Explosive: false,
PasswordHashing: false, PasswordHashing: false,
}, },
{
Name: "BLIND",
Arity: 2,
Output: 1,
Decompose: DecomposeRule{
HasRule: true,
Given: []int{0},
Reveal: 1,
Filter: func(p Primitive, x Value, i int) (Value, bool) {
return x, true
},
},
Recompose: RecomposeRule{
HasRule: false,
},
Rewrite: RewriteRule{
HasRule: false,
},
Rebuild: RebuildRule{
HasRule: false,
},
Check: false,
Injectable: true,
Explosive: false,
PasswordHashing: false,
},
{
Name: "UNBLIND",
Arity: 3,
Output: 1,
Decompose: DecomposeRule{
HasRule: false,
},
Recompose: RecomposeRule{
HasRule: false,
},
Rewrite: RewriteRule{
HasRule: true,
Name: "SIGN",
From: 2,
To: func(p Primitive) Value {
return Value{
Kind: "primitive",
Primitive: Primitive{
Name: "SIGN",
Arguments: []Value{
p.Arguments[0],
p.Arguments[1].Primitive.Arguments[1],
},
Output: 0,
Check: false,
},
}
},
Matching: map[int][]int{
0: {1},
},
Filter: func(p Primitive, x Value, i int) (Value, bool) {
switch i {
case 1:
blindPrim := Value{
Kind: "primitive",
Primitive: Primitive{
Name: "BLIND",
Arguments: []Value{
p.Arguments[0], p.Arguments[1],
},
Output: 0,
Check: false,
},
}
return blindPrim, true
}
return x, false
},
},
Rebuild: RebuildRule{
HasRule: false,
},
Check: false,
Injectable: true,
Explosive: false,
PasswordHashing: false,
},
} }
func primitiveIsCorePrim(name string) bool { func primitiveIsCorePrim(name string) bool {
......
...@@ -107,23 +107,23 @@ type DecomposeRule struct { ...@@ -107,23 +107,23 @@ type DecomposeRule struct {
HasRule bool HasRule bool
Given []int Given []int
Reveal int Reveal int
Filter func(Value, int) (Value, bool) Filter func(Primitive, Value, int) (Value, bool)
} }
type RecomposeRule struct { type RecomposeRule struct {
HasRule bool HasRule bool
Given [][]int Given [][]int
Reveal int Reveal int
Filter func(Value, int) (Value, bool) Filter func(Primitive, Value, int) (Value, bool)
} }
type RewriteRule struct { type RewriteRule struct {
HasRule bool HasRule bool
Name string Name string
From int From int
To int To func(Primitive) Value
Matching map[int][]int Matching map[int][]int
Filter func(Value, int) (Value, bool) Filter func(Primitive, Value, int) (Value, bool)
} }
type RebuildRule struct { type RebuildRule struct {
...@@ -131,7 +131,7 @@ type RebuildRule struct { ...@@ -131,7 +131,7 @@ type RebuildRule struct {
Name string Name string
Given [][]int Given [][]int
Reveal int Reveal int
Filter func(Value, int) (Value, bool) Filter func(Primitive, Value, int) (Value, bool)
} }
type PrimitiveCoreSpec struct { type PrimitiveCoreSpec struct {
......
...@@ -27,7 +27,7 @@ syn match verifpalDelim ")" ...@@ -27,7 +27,7 @@ syn match verifpalDelim ")"
syn match verifpalDelim "\[" syn match verifpalDelim "\["
syn match verifpalDelim "]" syn match verifpalDelim "]"
syn keyword verifpalKeywrd knows generates leaks syn keyword verifpalKeywrd knows generates leaks
syn keyword verifpalConstr RINGSIGNVERIF RINGSIGN PW_HASH HASH HKDF AEAD_ENC AEAD_DEC ENC DEC ASSERT CONCAT SPLIT MAC SIGNVERIF SIGN PKE_ENC PKE_DEC SHAMIR_SPLIT SHAMIR_JOIN G nil _ syn keyword verifpalConstr UNBLIND BLIND RINGSIGNVERIF RINGSIGN PW_HASH HASH HKDF AEAD_ENC AEAD_DEC ENC DEC ASSERT CONCAT SPLIT MAC SIGNVERIF SIGN PKE_ENC PKE_DEC SHAMIR_SPLIT SHAMIR_JOIN G nil _
syn match verifpalConstr "\^" syn match verifpalConstr "\^"
syn keyword verifpalDecl principal phase queries attacker confidentiality authentication freshness unlinkability precondition syn keyword verifpalDecl principal phase queries attacker confidentiality authentication freshness unlinkability precondition
syn match verifpalTransfer "->" syn match verifpalTransfer "->"
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment