diff --git a/examples/blind.vp b/examples/blind.vp new file mode 100644 index 0000000000000000000000000000000000000000..3e6ee859ffa71a592f08f2490f29191c868d3041 --- /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 bbfa4cc968c77c87fbbd811dbd5fbf0cdea21c3e..775c76a60d0ac999505a08c458c0104a8320c927 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 1c0056a7887ff9d500604ca19d26295e4cb5f1fe..2d476f929e721d520c2927c42a4e2a27fdf073d0 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 215c4617f904e392bffd2e53807928dc1b7fab4c..d7f263ebefc1b3cb2b4ddcaa8c3d448ae83d1f7a 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 fab7336ccabe5b903373cc4eec9dd0e656183722..798302bda0da45f844a6b8a67b315a881c42611b 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 "->"