From d2261c6b0daddbdccee9ef72e06604ede463d405 Mon Sep 17 00:00:00 2001 From: Nadim Kobeissi Date: Thu, 30 Apr 2020 09:15:18 +0200 Subject: [PATCH] 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. --- examples/blind.vp | 29 ++++++++ internal/verifpal/possible.go | 9 +-- internal/verifpal/primitive.go | 130 ++++++++++++++++++++++++++++----- internal/verifpal/types.go | 10 +-- tools/vim/syntax/verifpal.vim | 2 +- 5 files changed, 150 insertions(+), 30 deletions(-) create mode 100644 examples/blind.vp diff --git a/examples/blind.vp b/examples/blind.vp new file mode 100644 index 0000000..3e6ee85 --- /dev/null +++ b/examples/blind.vp @@ -0,0 +1,29 @@ +// SPDX-FileCopyrightText: © 2019-2020 Nadim Kobeissi +// 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 +] diff --git a/internal/verifpal/possible.go b/internal/verifpal/possible.go index bbfa4cc..775c76a 100755 --- a/internal/verifpal/possible.go +++ b/internal/verifpal/possible.go @@ -19,7 +19,7 @@ func possibleToDecomposePrimitive( } for i, g := range prim.Decompose.Given { a := p.Arguments[g] - a, valid := prim.Decompose.Filter(a, i) + a, valid := prim.Decompose.Filter(p, a, i) ii := sanityEquivalentValueInValues(a, valAttackerState.Known) if valid && ii >= 0 { has = append(has, a) @@ -197,10 +197,7 @@ func possibleToRewrite( if !possibleToRewritePrim(p, valPrincipalState) { return !prim.Check, v } - rewrite := Value{Kind: "primitive", Primitive: p} - if prim.Rewrite.To > 0 { - rewrite = from.Primitive.Arguments[prim.Rewrite.To] - } + rewrite := prim.Rewrite.To(from.Primitive) return true, []Value{rewrite} } return !prim.Check, v @@ -215,7 +212,7 @@ func possibleToRewritePrim( valid := false for _, mm := range m { 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 { continue } diff --git a/internal/verifpal/primitive.go b/internal/verifpal/primitive.go index 1c0056a..2d476f9 100755 --- a/internal/verifpal/primitive.go +++ b/internal/verifpal/primitive.go @@ -138,7 +138,7 @@ var primitiveSpecs = []PrimitiveSpec{ HasRule: true, Given: []int{0}, Reveal: 1, - Filter: func(x Value, i int) (Value, bool) { + Filter: func(p Primitive, x Value, i int) (Value, bool) { return x, true }, }, @@ -164,7 +164,7 @@ var primitiveSpecs = []PrimitiveSpec{ HasRule: true, Given: []int{0}, Reveal: 1, - Filter: func(x Value, i int) (Value, bool) { + Filter: func(p Primitive, x Value, i int) (Value, bool) { return x, true }, }, @@ -175,12 +175,14 @@ var primitiveSpecs = []PrimitiveSpec{ HasRule: true, Name: "AEAD_ENC", From: 1, - To: 1, + To: func(p Primitive) Value { + return p.Arguments[1] + }, Matching: map[int][]int{ 0: {0}, 2: {2}, }, - Filter: func(x Value, i int) (Value, bool) { + Filter: func(p Primitive, x Value, i int) (Value, bool) { switch i { case 0: return x, true @@ -206,7 +208,7 @@ var primitiveSpecs = []PrimitiveSpec{ HasRule: true, Given: []int{0}, Reveal: 1, - Filter: func(x Value, i int) (Value, bool) { + Filter: func(p Primitive, x Value, i int) (Value, bool) { return x, true }, }, @@ -232,7 +234,7 @@ var primitiveSpecs = []PrimitiveSpec{ HasRule: true, Given: []int{0}, Reveal: 1, - Filter: func(x Value, i int) (Value, bool) { + Filter: func(p Primitive, x Value, i int) (Value, bool) { return x, true }, }, @@ -243,11 +245,13 @@ var primitiveSpecs = []PrimitiveSpec{ HasRule: true, Name: "ENC", From: 1, - To: 1, + To: func(p Primitive) Value { + return p.Arguments[1] + }, Matching: map[int][]int{ 0: {0}, }, - Filter: func(x Value, i int) (Value, bool) { + Filter: func(p Primitive, x Value, i int) (Value, bool) { switch i { case 0: return x, true @@ -319,12 +323,14 @@ var primitiveSpecs = []PrimitiveSpec{ HasRule: true, Name: "SIGN", From: 2, - To: -1, + To: func(p Primitive) Value { + return constantN + }, Matching: map[int][]int{ 0: {0}, 1: {1}, }, - Filter: func(x Value, i int) (Value, bool) { + Filter: func(p Primitive, x Value, i int) (Value, bool) { switch i { case 0: switch x.Kind { @@ -362,7 +368,7 @@ var primitiveSpecs = []PrimitiveSpec{ HasRule: true, Given: []int{0}, Reveal: 1, - Filter: func(x Value, i int) (Value, bool) { + Filter: func(p Primitive, x Value, i int) (Value, bool) { switch i { case 0: switch x.Kind { @@ -404,7 +410,7 @@ var primitiveSpecs = []PrimitiveSpec{ HasRule: true, Given: []int{0}, Reveal: 1, - Filter: func(x Value, i int) (Value, bool) { + Filter: func(p Primitive, x Value, i int) (Value, bool) { return x, true }, }, @@ -415,11 +421,13 @@ var primitiveSpecs = []PrimitiveSpec{ HasRule: true, Name: "PKE_ENC", From: 1, - To: 1, + To: func(p Primitive) Value { + return p.Arguments[1] + }, Matching: map[int][]int{ 0: {0}, }, - Filter: func(x Value, i int) (Value, bool) { + Filter: func(p Primitive, x Value, i int) (Value, bool) { switch i { case 0: switch x.Kind { @@ -460,7 +468,7 @@ var primitiveSpecs = []PrimitiveSpec{ {1, 2}, }, Reveal: 0, - Filter: func(x Value, i int) (Value, bool) { + Filter: func(p Primitive, x Value, i int) (Value, bool) { return x, true }, }, @@ -500,7 +508,7 @@ var primitiveSpecs = []PrimitiveSpec{ {2, 1}, }, Reveal: 0, - Filter: func(x Value, i int) (Value, bool) { + Filter: func(p Primitive, x Value, i int) (Value, bool) { return x, true }, }, @@ -544,14 +552,16 @@ var primitiveSpecs = []PrimitiveSpec{ HasRule: true, Name: "RINGSIGN", From: 4, - To: -1, + To: func(p Primitive) Value { + return constantN + }, Matching: map[int][]int{ 0: {0, 1, 2}, 1: {0, 1, 2}, 2: {0, 1, 2}, 3: {3}, }, - Filter: func(x Value, i int) (Value, bool) { + Filter: func(p Primitive, x Value, i int) (Value, bool) { switch i { case 0: switch x.Kind { @@ -587,6 +597,90 @@ var primitiveSpecs = []PrimitiveSpec{ Explosive: 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 { diff --git a/internal/verifpal/types.go b/internal/verifpal/types.go index 215c461..d7f263e 100755 --- a/internal/verifpal/types.go +++ b/internal/verifpal/types.go @@ -107,23 +107,23 @@ type DecomposeRule struct { HasRule bool Given []int Reveal int - Filter func(Value, int) (Value, bool) + Filter func(Primitive, Value, int) (Value, bool) } type RecomposeRule struct { HasRule bool Given [][]int Reveal int - Filter func(Value, int) (Value, bool) + Filter func(Primitive, Value, int) (Value, bool) } type RewriteRule struct { HasRule bool Name string From int - To int + To func(Primitive) Value Matching map[int][]int - Filter func(Value, int) (Value, bool) + Filter func(Primitive, Value, int) (Value, bool) } type RebuildRule struct { @@ -131,7 +131,7 @@ type RebuildRule struct { Name string Given [][]int Reveal int - Filter func(Value, int) (Value, bool) + Filter func(Primitive, Value, int) (Value, bool) } type PrimitiveCoreSpec struct { diff --git a/tools/vim/syntax/verifpal.vim b/tools/vim/syntax/verifpal.vim index fab7336..798302b 100755 --- a/tools/vim/syntax/verifpal.vim +++ b/tools/vim/syntax/verifpal.vim @@ -27,7 +27,7 @@ syn match verifpalDelim ")" syn match verifpalDelim "\[" syn match verifpalDelim "]" 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 keyword verifpalDecl principal phase queries attacker confidentiality authentication freshness unlinkability precondition syn match verifpalTransfer "->" -- GitLab