Skip to content

GitLab

Commit 2ac01923 authored by Nadim Kobeissi's avatar Nadim Kobeissi 💾
Browse files

Simplify equivalence resolution fix

parent 25e545a9
Pipeline #915 passed with stages
in 2 minutes and 50 seconds
Hide whitespace changes
Inline Side-by-side
cmd/verifpal/main_test.go
View file @ 2ac01923
......@@ -16,7 +16,7 @@ type VerifpalTest struct {
ResultsCode string
}
var verifpalTests = [57]VerifpalTest{
var verifpalTests = [58]VerifpalTest{
{
Model: "challengeresponse.vp",
ResultsCode: "a0a1",
......@@ -267,6 +267,10 @@ var verifpalTests = [57]VerifpalTest{
Model: "melanie_bugs.vp",
ResultsCode: "c1c1c1c1c1a1",
},
{
Model: "simple_equiv.vp",
ResultsCode: "e0",
},
}
func TestMain(t *testing.T) {
......
cmd/vplogic/inject.go
View file @ 2ac01923
......@@ -194,7 +194,7 @@ func injectPrimitive(
for _, k := range valAttackerState.Known {
switch k.Kind {
case typesEnumConstant:
k, _ = valueResolveConstant(k.Data.(*Constant), valPrincipalState)
k, _ = valueResolveConstant(k.Data.(*Constant), valPrincipalState, true)
}
if !injectValueRules(k, arg, p, stage) {
continue
......
cmd/vplogic/mutationmap.go
View file @ 2ac01923
......@@ -32,7 +32,7 @@ func mutationMapInit(
case typesEnumEquation:
continue
}
a, i := valueResolveConstant(v.Data.(*Constant), valPrincipalState)
a, i := valueResolveConstant(v.Data.(*Constant), valPrincipalState, true)
if mutationMapSkipValue(v, i, valKnowledgeMap, valPrincipalState, valAttackerState) {
continue
}
......@@ -122,7 +122,7 @@ func mutationMapReplaceConstant(
if valueIsGOrNil(v.Data.(*Constant)) {
continue
}
c, _ := valueResolveConstant(v.Data.(*Constant), valPrincipalState)
c, _ := valueResolveConstant(v.Data.(*Constant), valPrincipalState, true)
switch c.Kind {
case typesEnumConstant:
if valueEquivalentValueInValues(c, mutations) < 0 {
......@@ -145,7 +145,7 @@ func mutationMapReplacePrimitive(
if valueIsGOrNil(v.Data.(*Constant)) {
continue
}
c, _ := valueResolveConstant(v.Data.(*Constant), valPrincipalState)
c, _ := valueResolveConstant(v.Data.(*Constant), valPrincipalState, true)
switch c.Kind {
case typesEnumConstant:
if valueEquivalentValueInValues(c, mutations) < 0 {
......
cmd/vplogic/possible.go
View file @ 2ac01923
......@@ -291,7 +291,7 @@ func possibleToObtainPasswords(
passwords := []*Value{}
switch a.Kind {
case typesEnumConstant:
aa, _ := valueResolveConstant(a.Data.(*Constant), valPrincipalState)
aa, _ := valueResolveConstant(a.Data.(*Constant), valPrincipalState, true)
switch aa.Kind {
case typesEnumConstant:
if aa.Data.(*Constant).Qualifier == typesEnumPassword {
......
cmd/vplogic/query.go
View file @ 2ac01923
......@@ -104,7 +104,7 @@ func queryAuthenticationGetPassIndices(
query Query, valKnowledgeMap *KnowledgeMap, valPrincipalState *PrincipalState,
) ([]int, principalEnum, *Constant) {
indices := []int{}
_, i := valueResolveConstant(query.Message.Constants[0], valPrincipalState)
_, i := valueResolveConstant(query.Message.Constants[0], valPrincipalState, true)
if i < 0 {
return indices, 0, &Constant{}
}
......@@ -129,7 +129,7 @@ func queryAuthenticationGetPassIndices(
if !valueFindConstantInPrimitiveFromKnowledgeMap(c, a, valKnowledgeMap) {
continue
}
_, iiii := valueResolveConstant(valKnowledgeMap.Constants[iii], valPrincipalState)
_, iiii := valueResolveConstant(valKnowledgeMap.Constants[iii], valPrincipalState, true)
if iiii < 0 {
return indices, sender, c
}
......@@ -157,7 +157,7 @@ func queryAuthenticationHandlePass(
result VerifyResult, c *Constant, b *Value, mutatedInfo string, sender principalEnum,
valPrincipalState *PrincipalState,
) VerifyResult {
cc, _ := valueResolveConstant(c, valPrincipalState)
cc, _ := valueResolveConstant(c, valPrincipalState, true)
result.Summary = infoVerifyResultSummary(mutatedInfo, fmt.Sprintf(
"%s (%s), sent by %s and not by %s, is successfully used in %s within %s's state.",
prettyConstant(c), prettyValue(cc), principalGetNameFromID(sender),
......@@ -204,7 +204,7 @@ func queryFreshness(
if !valueFindConstantInPrimitiveFromKnowledgeMap(query.Constants[0], a, valKnowledgeMap) {
continue
}
_, ii := valueResolveConstant(valKnowledgeMap.Constants[i], valPrincipalState)
_, ii := valueResolveConstant(valKnowledgeMap.Constants[i], valPrincipalState, true)
if ii < 0 {
return result, nil
}
......@@ -228,7 +228,7 @@ func queryFreshness(
if len(indices) == 0 {
return result, nil
}
resolved, _ := valueResolveConstant(query.Constants[0], valPrincipalState)
resolved, _ := valueResolveConstant(query.Constants[0], valPrincipalState, true)
mutatedInfo := infoQueryMutatedValues(
valKnowledgeMap, valPrincipalState, valAttackerState, resolved, 0,
)
......@@ -277,7 +277,7 @@ func queryUnlinkability(
}
}
if len(noFreshness) > 0 {
resolved, _ := valueResolveConstant(noFreshness[0], valPrincipalState)
resolved, _ := valueResolveConstant(noFreshness[0], valPrincipalState, true)
mutatedInfo := infoQueryMutatedValues(
valKnowledgeMap, valPrincipalState, valAttackerState, resolved, 0,
)
......@@ -298,7 +298,7 @@ func queryUnlinkability(
constants := []*Constant{}
assigneds := []*Value{}
for i := 0; i < len(query.Constants); i++ {
a, _ := valueResolveConstant(query.Constants[i], valPrincipalState)
a, _ := valueResolveConstant(query.Constants[i], valPrincipalState, true)
constants = append(constants, query.Constants[i])
assigneds = append(assigneds, a)
}
......@@ -355,7 +355,7 @@ func queryEquivalence(
}
values := []*Value{}
for i := 0; i < len(query.Constants); i++ {
a, _ := valueResolveConstantEqv(query.Constants[i], valPrincipalState)
a, _ := valueResolveConstant(query.Constants[i], valPrincipalState, false)
values = append(values, a)
}
brokenEquivalence := false
......@@ -406,7 +406,7 @@ func queryPrecondition(
Summary: "",
}
recipientKnows := false
_, i := valueResolveConstant(option.Message.Constants[0], valPrincipalState)
_, i := valueResolveConstant(option.Message.Constants[0], valPrincipalState, true)
if i < 0 {
result.Options = append(result.Options, oResult)
continue
......
cmd/vplogic/value.go
View file @ 2ac01923
......@@ -463,25 +463,17 @@ func valueShouldResolveToBeforeMutate(i int, valPrincipalState *PrincipalState)
return false
}
func valueResolveConstant(c *Constant, valPrincipalState *PrincipalState) (*Value, int) {
func valueResolveConstant(c *Constant, valPrincipalState *PrincipalState, allowBeforeMutate bool) (*Value, int) {
i := valueGetPrincipalStateIndexFromConstant(valPrincipalState, c)
if i < 0 {
return &Value{Kind: typesEnumConstant, Data: c}, i
}
if valueShouldResolveToBeforeMutate(i, valPrincipalState) {
if allowBeforeMutate && valueShouldResolveToBeforeMutate(i, valPrincipalState) {
return valPrincipalState.BeforeMutate[i], i
}
return valPrincipalState.Assigned[i], i
}
func valueResolveConstantEqv(c *Constant, valPrincipalState *PrincipalState) (*Value, int) {
i := valueGetPrincipalStateIndexFromConstant(valPrincipalState, c)
if i < 0 {
return &Value{Kind: typesEnumConstant, Data: c}, i
}
return valPrincipalState.Assigned[i], i
}
func valueResolveValueInternalValuesFromKnowledgeMap(
a *Value, valKnowledgeMap *KnowledgeMap,
) (*Value, []*Value) {
......@@ -609,7 +601,7 @@ func valueResolveValueInternalValuesFromPrincipalState(
if forceBeforeMutate {
a = valPrincipalState.BeforeMutate[nextRootIndex]
} else {
a, _ = valueResolveConstant(a.Data.(*Constant), valPrincipalState)
a, _ = valueResolveConstant(a.Data.(*Constant), valPrincipalState, true)
}
default:
switch rootValue.Kind {
......@@ -698,7 +690,7 @@ func valueResolveEquationInternalValuesFromPrincipalState(
switch aa[aai].Kind {
case typesEnumConstant:
var i int
aa[aai], i = valueResolveConstant(aa[aai].Data.(*Constant), valPrincipalState)
aa[aai], i = valueResolveConstant(aa[aai].Data.(*Constant), valPrincipalState, true)
if forceBeforeMutate {
aa[aai] = valPrincipalState.BeforeMutate[i]
}
......
cmd/vplogic/verifyactive.go
View file @ 2ac01923
......@@ -144,7 +144,7 @@ func verifyActiveMutatePrincipalState(
earliestMutation := len(valPrincipalState.Constants)
isWorthwhileMutation := false
for i := 0; i < len(valMutationMap.Constants); i++ {
ai, ii := valueResolveConstant(valMutationMap.Constants[i], valPrincipalState)
ai, ii := valueResolveConstant(valMutationMap.Constants[i], valPrincipalState, true)
ac := valMutationMap.Combination[i]
ar, _ := valueResolveValueInternalValuesFromKnowledgeMap(ai, valKnowledgeMap)
switch ac.Kind {
......
cmd/vplogic/verifyanalysis.go
View file @ 2ac01923
......@@ -153,7 +153,7 @@ func verifyAnalysisEquivalize(a *Value, valPrincipalState *PrincipalState) int {
ar := a
switch a.Kind {
case typesEnumConstant:
ar, _ = valueResolveConstant(a.Data.(*Constant), valPrincipalState)
ar, _ = valueResolveConstant(a.Data.(*Constant), valPrincipalState, true)
}
for i := 0; i < len(valPrincipalState.Assigned); i++ {
if valueEquivalentValues(ar, valPrincipalState.Assigned[i], true) {
......
examples/test/mwe.vp
View file @ 2ac01923
// SPDX-FileCopyrightText: © 2019-2021 Nadim Kobeissi <nadim@symbolic.software>
// SPDX-License-Identifier: GPL-3.0-only
attacker[passive]
principal Alice[
......
examples/test/replay-simple.vp
View file @ 2ac01923
// SPDX-FileCopyrightText: © 2019-2021 Nadim Kobeissi <nadim@symbolic.software>
// SPDX-License-Identifier: GPL-3.0-only
attacker[active]
principal Alice[
......
examples/test/simple_equiv.vp 0 → 100644
View file @ 2ac01923
// SPDX-FileCopyrightText: © 2019-2021 Nadim Kobeissi <nadim@symbolic.software>
// SPDX-License-Identifier: GPL-3.0-only
attacker[passive]
principal Server[
generates x
generates y
gx = G^x
gy = G^y
gxy = gx^y
gyx = gy^x
]
queries [
equivalence? gxy, gyx
]
go.mod
View file @ 2ac01923
......@@ -8,11 +8,12 @@ go 1.16
require (
github.com/akavel/rsrc v0.10.2 // indirect
github.com/inconshreveable/mousetrap v1.0.0 // indirect
github.com/josephspurrier/goversioninfo v1.2.0 // indirect
github.com/josephspurrier/goversioninfo v1.3.0 // indirect
github.com/logrusorgru/aurora v2.0.3+incompatible
github.com/mna/pigeon v1.1.0 // indirect
github.com/spf13/cobra v1.2.1
github.com/spf13/pflag v1.0.5 // indirect
golang.org/x/sys v0.0.0-20210630005230-0f9fa26af87c // indirect
golang.org/x/tools v0.1.4 // indirect
golang.org/x/mod v0.5.0 // indirect
golang.org/x/sys v0.0.0-20210817134402-fefb4affbef3 // indirect
golang.org/x/tools v0.1.5 // indirect
)
go.sum
View file @ 2ac01923
......@@ -186,6 +186,8 @@ github.com/inconshreveable/mousetrap v1.0.0/go.mod h1:PxqpIevigyE2G7u3NXJIT2ANyt
github.com/jonboulle/clockwork v0.1.0/go.mod h1:Ii8DK3G1RaLaWxj9trq07+26W01tbo22gdxWY5EU2bo=
github.com/josephspurrier/goversioninfo v1.2.0 h1:tpLHXAxLHKHg/dCU2AAYx08A4m+v9/CWg6+WUvTF4uQ=
github.com/josephspurrier/goversioninfo v1.2.0/go.mod h1:AGP2a+Y/OVJZ+s6XM4IwFUpkETwvn0orYurY8qpw1+0=
github.com/josephspurrier/goversioninfo v1.3.0 h1:pmgDhWnG8I59p5kCR09J73s/gy9JqRPAtiaUK8jixtE=
github.com/josephspurrier/goversioninfo v1.3.0/go.mod h1:JWzv5rKQr+MmW+LvM412ToT/IkYDZjaclF2pKDss8IY=
github.com/json-iterator/go v1.1.11/go.mod h1:KdQUCv79m/52Kvf8AW2vK1V8akMuk1QjK/uOdHXbAo4=
github.com/jstemmer/go-junit-report v0.0.0-20190106144839-af01ea7f8024/go.mod h1:6v2b51hI/fHJwM22ozAgKL4VKDeJcHhJFhtBdhmNjmU=
github.com/jstemmer/go-junit-report v0.9.1/go.mod h1:Brl9GWCQeLvo8nXZwPNNblvFj/XSXhF0NWZEnDohbsk=
......@@ -335,6 +337,8 @@ golang.org/x/mod v0.4.0/go.mod h1:s0Qsj1ACt9ePp/hMypM3fl4fZqREWJwdYDEqhRiZZUA=
golang.org/x/mod v0.4.1/go.mod h1:s0Qsj1ACt9ePp/hMypM3fl4fZqREWJwdYDEqhRiZZUA=
golang.org/x/mod v0.4.2 h1:Gz96sIWK3OalVv/I/qNygP42zyoKp3xptRVCWRFEBvo=
golang.org/x/mod v0.4.2/go.mod h1:s0Qsj1ACt9ePp/hMypM3fl4fZqREWJwdYDEqhRiZZUA=
golang.org/x/mod v0.5.0 h1:UG21uOlmZabA4fW5i7ZX6bjw1xELEGg/ZLgZq9auk/Q=
golang.org/x/mod v0.5.0/go.mod h1:5OXOZSfqPIIbmVBIIKWRFfZjPR0E5r58TLhUjH0a2Ro=
golang.org/x/net v0.0.0-20180724234803-3673e40ba225/go.mod h1:mL1N/T3taQHkDXs73rZJwtUhF3w3ftmwwsq0BUmARs4=
golang.org/x/net v0.0.0-20180826012351-8a410e7b638d/go.mod h1:mL1N/T3taQHkDXs73rZJwtUhF3w3ftmwwsq0BUmARs4=
golang.org/x/net v0.0.0-20181023162649-9b4f9f5ad519/go.mod h1:mL1N/T3taQHkDXs73rZJwtUhF3w3ftmwwsq0BUmARs4=
......@@ -443,6 +447,8 @@ golang.org/x/sys v0.0.0-20210510120138-977fb7262007/go.mod h1:oPkhp1MJrh7nUepCBc
golang.org/x/sys v0.0.0-20210611083646-a4fc73990273/go.mod h1:oPkhp1MJrh7nUepCBck5+mAzfO9JrbApNNgaTdGDITg=
golang.org/x/sys v0.0.0-20210630005230-0f9fa26af87c h1:F1jZWGFhYfh0Ci55sIpILtKKK8p3i2/krTr0H1rg74I=
golang.org/x/sys v0.0.0-20210630005230-0f9fa26af87c/go.mod h1:oPkhp1MJrh7nUepCBck5+mAzfO9JrbApNNgaTdGDITg=
golang.org/x/sys v0.0.0-20210817134402-fefb4affbef3 h1:VU4cjb3pNZovHYRs/2E8zPrpLC05+GT2uqqgIFtt0jc=
golang.org/x/sys v0.0.0-20210817134402-fefb4affbef3/go.mod h1:oPkhp1MJrh7nUepCBck5+mAzfO9JrbApNNgaTdGDITg=
golang.org/x/term v0.0.0-20201126162022-7de9c90e9dd1/go.mod h1:bj7SfCRtBDWHUb9snDiAeCFNEtKQo2Wmx5Cou7ajbmo=
golang.org/x/text v0.0.0-20170915032832-14c0d48ead0c/go.mod h1:NqM8EUOU14njkJ3fqMW+pc6Ldnwhi/IjpwHt7yyuwOQ=
golang.org/x/text v0.3.0/go.mod h1:NqM8EUOU14njkJ3fqMW+pc6Ldnwhi/IjpwHt7yyuwOQ=
......@@ -509,6 +515,8 @@ golang.org/x/tools v0.1.2/go.mod h1:o0xws9oXOQQZyjljx8fwUC0k7L1pTE6eaCbjGeHmOkk=
golang.org/x/tools v0.1.3/go.mod h1:o0xws9oXOQQZyjljx8fwUC0k7L1pTE6eaCbjGeHmOkk=
golang.org/x/tools v0.1.4 h1:cVngSRcfgyZCzys3KYOpCFa+4dqX/Oub9tAq00ttGVs=
golang.org/x/tools v0.1.4/go.mod h1:o0xws9oXOQQZyjljx8fwUC0k7L1pTE6eaCbjGeHmOkk=
golang.org/x/tools v0.1.5 h1:ouewzE6p+/VEB31YYnTbEJdi8pFqKp4P4n85vwo3DHA=
golang.org/x/tools v0.1.5/go.mod h1:o0xws9oXOQQZyjljx8fwUC0k7L1pTE6eaCbjGeHmOkk=
golang.org/x/xerrors v0.0.0-20190717185122-a985d3407aa7/go.mod h1:I/5z698sn9Ka8TeJc9MKroUUfqBBauWjQqLJ2OPfmY0=
golang.org/x/xerrors v0.0.0-20191011141410-1b5146add898/go.mod h1:I/5z698sn9Ka8TeJc9MKroUUfqBBauWjQqLJ2OPfmY0=
golang.org/x/xerrors v0.0.0-20191204190536-9bdfabe68543/go.mod h1:I/5z698sn9Ka8TeJc9MKroUUfqBBauWjQqLJ2OPfmY0=
......
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