Unverified Commit fbc4d737 authored by Nadim Kobeissi's avatar Nadim Kobeissi 💎

RINGSIGN and RINGSIGNVERIF (experimental)

As suggested by Sebastian R. Verschoor:
https://lists.symbolic.software/pipermail/verifpal/2020/000157.html
parent dbdbad6e
......@@ -25,7 +25,7 @@ import (
var parserReserved = []string{
"attacker", "passive", "active", "principal",
"phase, public", "private", "password",
"confidentiality", "authentication", "precondition",
"confidentiality", "authentication", "precondition", "ringsign", "ringsignverif",
"primitive", "pw_hash", "hash", "hkdf",
"aead_enc", "aead_dec", "enc", "dec",
"mac", "assert", "sign", "signverif",
......
......@@ -42,7 +42,7 @@ func attackerStateAbsorbPhaseValues(valPrincipalState principalState) {
attackerStateShared.mutatedTo = append(attackerStateShared.mutatedTo, []string{})
}
for i, c := range valPrincipalState.constants {
if !valPrincipalState.wire[i] && !valPrincipalState.constants[i].leaked {
if !strInSlice(valPrincipalState.name, valPrincipalState.wire[i]) && !valPrincipalState.constants[i].leaked {
continue
}
if valPrincipalState.constants[i].qualifier != "private" {
......
......@@ -325,7 +325,7 @@ func constructPrincipalStates(m Model, valKnowledgeMap knowledgeMap) []principal
assigned: []value{},
guard: []bool{},
known: []bool{},
wire: []bool{},
wire: [][]string{},
knownBy: [][]map[string]string{},
creator: []string{},
sender: []string{},
......@@ -339,7 +339,7 @@ func constructPrincipalStates(m Model, valKnowledgeMap knowledgeMap) []principal
for i, c := range valKnowledgeMap.constants {
guard := false
knows := false
wire := false
wire := []string{}
sender := valKnowledgeMap.creator[i]
assigned := valKnowledgeMap.assigned[i]
if valKnowledgeMap.creator[i] == principal {
......@@ -352,17 +352,17 @@ func constructPrincipalStates(m Model, valKnowledgeMap knowledgeMap) []principal
break
}
}
BlocksLoop:
for _, blck := range m.blocks {
switch blck.kind {
case "message":
roc := ((blck.message.recipient == principal) ||
(valKnowledgeMap.creator[i] == principal))
ir := (blck.message.recipient == principal)
ic := (valKnowledgeMap.creator[i] == principal)
for _, cc := range blck.message.constants {
if c.name == cc.name {
wire = true
guard = cc.guard && roc
break BlocksLoop
wire = append(wire, principal)
if !guard {
guard = cc.guard && (ir || ic)
}
}
}
}
......@@ -393,7 +393,7 @@ func constructPrincipalStateClone(valPrincipalState principalState, purify bool)
assigned: make([]value, len(valPrincipalState.assigned)),
guard: make([]bool, len(valPrincipalState.guard)),
known: make([]bool, len(valPrincipalState.known)),
wire: make([]bool, len(valPrincipalState.wire)),
wire: make([][]string, len(valPrincipalState.wire)),
knownBy: make([][]map[string]string, len(valPrincipalState.knownBy)),
creator: make([]string, len(valPrincipalState.creator)),
sender: make([]string, len(valPrincipalState.sender)),
......
This diff is collapsed.
......@@ -205,12 +205,28 @@ func possibleToRewrite(
if from.primitive.name != prim.rewrite.name {
return (false || !prim.check), value{kind: "primitive", primitive: p}
}
for _, m := range prim.rewrite.matching {
var valid bool
ax := []value{p.arguments[m], from.primitive.arguments[m]}
ax[0], valid = prim.rewrite.filter(ax[0], m, valPrincipalState)
if !possibleToRewritePrim(p, valPrincipalState) {
return (false || !prim.check), value{kind: "primitive", primitive: p}
}
rewrite := value{kind: "primitive", primitive: p}
if prim.rewrite.to > 0 {
rewrite = from.primitive.arguments[prim.rewrite.to]
}
return true, rewrite
}
return (false || !prim.check), value{kind: "primitive", primitive: p}
}
func possibleToRewritePrim(p primitive, valPrincipalState principalState) bool {
prim := primitiveGet(p.name)
from := p.arguments[prim.rewrite.from]
for a, m := range prim.rewrite.matching {
valid := false
for _, mm := range m {
ax := []value{p.arguments[a], from.primitive.arguments[mm]}
ax[0], valid = prim.rewrite.filter(ax[0], mm, valPrincipalState)
if !valid {
return (false || !prim.check), value{kind: "primitive", primitive: p}
continue
}
for i := range ax {
switch ax[i].kind {
......@@ -221,17 +237,16 @@ func possibleToRewrite(
}
}
}
if !sanityEquivalentValues(ax[0], ax[1], valPrincipalState) {
return (false || !prim.check), value{kind: "primitive", primitive: p}
valid = sanityEquivalentValues(ax[0], ax[1], valPrincipalState)
if valid {
break
}
}
rewrite := value{kind: "primitive", primitive: p}
if prim.rewrite.to > 0 {
rewrite = from.primitive.arguments[prim.rewrite.to]
if !valid {
return false
}
return true, rewrite
}
return (false || !prim.check), value{kind: "primitive", primitive: p}
return true
}
func possibleToForceRewrite(p primitive, valPrincipalState principalState, valAttackerState attackerState) bool {
......
......@@ -108,11 +108,14 @@ var primitiveSpecs = []primitiveSpec{
hasRule: false,
},
rewrite: rewriteRule{
hasRule: true,
name: "AEAD_ENC",
from: 1,
to: 1,
matching: []int{0, 2},
hasRule: true,
name: "AEAD_ENC",
from: 1,
to: 1,
matching: map[int][]int{
0: {0},
2: {2},
},
filter: func(x value, i int, valPrincipalState principalState) (value, bool) {
switch i {
case 0:
......@@ -171,11 +174,13 @@ var primitiveSpecs = []primitiveSpec{
hasRule: false,
},
rewrite: rewriteRule{
hasRule: true,
name: "ENC",
from: 1,
to: 1,
matching: []int{0},
hasRule: true,
name: "ENC",
from: 1,
to: 1,
matching: map[int][]int{
0: {0},
},
filter: func(x value, i int, valPrincipalState principalState) (value, bool) {
switch i {
case 0:
......@@ -263,11 +268,14 @@ var primitiveSpecs = []primitiveSpec{
hasRule: false,
},
rewrite: rewriteRule{
hasRule: true,
name: "SIGN",
from: 2,
to: -1,
matching: []int{0, 1},
hasRule: true,
name: "SIGN",
from: 2,
to: -1,
matching: map[int][]int{
0: {0},
1: {1},
},
filter: func(x value, i int, valPrincipalState principalState) (value, bool) {
switch i {
case 0:
......@@ -278,13 +286,14 @@ var primitiveSpecs = []primitiveSpec{
return x, false
case "equation":
values := sanityDecomposeEquationValues(
x.equation,
valPrincipalState,
x.equation, valPrincipalState,
)
if len(values) == 2 {
switch len(values) {
case 2:
return values[1], true
default:
return x, false
}
return x, false
}
case 1:
return x, true
......@@ -360,11 +369,13 @@ var primitiveSpecs = []primitiveSpec{
hasRule: false,
},
rewrite: rewriteRule{
hasRule: true,
name: "PKE_ENC",
from: 1,
to: 1,
matching: []int{0},
hasRule: true,
name: "PKE_ENC",
from: 1,
to: 1,
matching: map[int][]int{
0: {0},
},
filter: func(x value, i int, valPrincipalState principalState) (value, bool) {
switch i {
case 0:
......@@ -452,6 +463,86 @@ var primitiveSpecs = []primitiveSpec{
injectable: false,
passwordHashing: false,
},
{
name: "RINGSIGN",
arity: 4,
output: 1,
decompose: decomposeRule{
hasRule: false,
},
recompose: recomposeRule{
hasRule: false,
},
rewrite: rewriteRule{
hasRule: false,
},
rebuild: rebuildRule{
hasRule: false,
},
check: false,
injectable: true,
passwordHashing: false,
},
{
name: "RINGSIGNVERIF",
arity: 5,
output: 1,
decompose: decomposeRule{
hasRule: false,
},
recompose: recomposeRule{
hasRule: false,
},
rewrite: rewriteRule{
hasRule: true,
name: "RINGSIGN",
from: 4,
to: -1,
matching: map[int][]int{
0: {0, 1, 2},
1: {0, 1, 2},
2: {0, 1, 2},
3: {3},
},
filter: func(x value, i int, valPrincipalState principalState) (value, bool) {
switch i {
case 0:
switch x.kind {
case "constant":
return x, false
case "primitive":
return x, false
case "equation":
values := sanityDecomposeEquationValues(
x.equation,
valPrincipalState,
)
switch len(values) {
case 2:
return values[1], true
default:
return x, false
}
}
case 1:
return x, true
case 2:
return x, true
case 3:
return x, true
case 4:
return x, true
}
return x, false
},
},
rebuild: rebuildRule{
hasRule: false,
},
check: true,
injectable: false,
passwordHashing: false,
},
}
func primitiveGet(name string) primitiveSpec {
......
......@@ -5,6 +5,7 @@
package verifpal
import (
"fmt"
"sync"
)
......@@ -25,6 +26,7 @@ func replacementMapInit(valPrincipalState principalState, valAttackerState attac
continue
}
a := valPrincipalState.assigned[ii]
fmt.Println(prettyValue(v))
replacementsGroup.Add(1)
go func(v value) {
c, r := replacementMapReplaceValue(
......@@ -63,6 +65,8 @@ func replacementMapSkipValue(
switch {
case !valAttackerState.wire[i]:
return true
case !strInSlice(valPrincipalState.name, valPrincipalState.wire[ii]):
return true
case valPrincipalState.guard[ii]:
iii := sanityGetAttackerStateIndexFromConstant(
valAttackerState, v.constant,
......
......@@ -123,7 +123,7 @@ type rewriteRule struct {
name string
from int
to int
matching []int
matching map[int][]int
filter func(value, int, principalState) (value, bool)
}
......@@ -154,7 +154,7 @@ type principalState struct {
assigned []value
guard []bool
known []bool
wire []bool
wire [][]string
knownBy [][]map[string]string
creator []string
sender []string
......
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