diff --git a/cmd/vplogic/primitive.go b/cmd/vplogic/primitive.go index cde669639503a9b6c36c31fa64d35cbb06bf818c..f704608e633fcae4404b0831359703353645dcee 100644 --- a/cmd/vplogic/primitive.go +++ b/cmd/vplogic/primitive.go @@ -17,7 +17,7 @@ var primitiveCoreSpecs = []PrimitiveCoreSpec{ CoreRule: func(p Primitive) (bool, []Value) { v := []Value{{Kind: "primitive", Primitive: p}} if valueEquivalentValues(p.Arguments[0], p.Arguments[1], true) { - return true, []Value{p.Arguments[0]} + return true, v } return false, v }, diff --git a/cmd/vplogic/verifyanalysis.go b/cmd/vplogic/verifyanalysis.go index 2f71e1924fb3a71098f1681c262f37e0fc7b0e6d..1f0439cca0ac288bf83fb08e7dbf89b2325bdaa4 100644 --- a/cmd/vplogic/verifyanalysis.go +++ b/cmd/vplogic/verifyanalysis.go @@ -96,8 +96,10 @@ func verifyAnalysisReconstruct( ) int { r := false ar := []Value{} + isCorePrim := false switch a.Kind { case "primitive": + isCorePrim = primitiveIsCorePrim(a.Primitive.Name) r, ar = possibleToReconstructPrimitive(a.Primitive, valAttackerState) for _, aa := range a.Primitive.Arguments { verifyAnalysisReconstruct(aa, valPrincipalState, valAttackerState, o) @@ -105,7 +107,7 @@ func verifyAnalysisReconstruct( case "equation": r, ar = possibleToReconstructEquation(a.Equation, valAttackerState) } - if r && attackerStatePutWrite(a) { + if r && !isCorePrim && attackerStatePutWrite(a) { InfoMessage(fmt.Sprintf( "%s obtained by reconstructing with %s.", infoOutputText(a), prettyValues(ar),