From 7e44096433bdff78d9e1c6a3b4d7d51b79870442 Mon Sep 17 00:00:00 2001
From: Nadim Kobeissi <nadim@symbolic.software>
Date: Mon, 13 Jul 2020 09:24:40 +0200
Subject: [PATCH] Don't reconstruct core primitives into attackerState

---
 cmd/vplogic/primitive.go      | 2 +-
 cmd/vplogic/verifyanalysis.go | 4 +++-
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/cmd/vplogic/primitive.go b/cmd/vplogic/primitive.go
index cde6696..f704608 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 2f71e19..1f0439c 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),
-- 
GitLab