Fix false attacks in authentication queries by rewriting primitives a…

…nd checking later for equivalence

The commit bcefa45 was added to address
some false attacks in
https://lists.symbolic.software/pipermail/verifpal/2020/000299.html, but
was reverted by the "Cleanup" commit
35e0a28.

The necessary lines seem to be in verifyActiveMutatePrincipalState in
cmd/vplogic/verifyactive.go. The code in the email fails after the
cleanup commit was added, but doesn't fail before the cleanup commit.

To test, use the code in
https://verifhub.verifpal.com/45ae1e65ce5ea647a2985bb098dc35e4 and
modify it so that bob uses the done message after it is received.

cmd/vplogic/verifyactive.go

@@ -147,18 +147,27 @@ func verifyActiveMutatePrincipalState(
 		ai, ii := valueResolveConstant(valMutationMap.Constants[i], valPrincipalState, true)
 		ac := valMutationMap.Combination[i]
 		ar, _ := valueResolveValueInternalValuesFromKnowledgeMap(ai, valKnowledgeMap)
+		switch ar.Kind {
+		case typesEnumPrimitive:
+		        _, aar := possibleToRewrite(ar.Data.(*Primitive), valPrincipalState)
+		        switch aar[0].Kind {
+		        case typesEnumPrimitive:
+		                ar.Data = aar[0].Data.(*Primitive)
+		        }
+		}
 		switch ac.Kind {
 		case typesEnumPrimitive:
+			_, aac := possibleToRewrite(ac.Data.(*Primitive), valPrincipalState)
+			switch aac[0].Kind {
+			case typesEnumPrimitive:
+				ac.Data = aac[0].Data.(*Primitive)
+			}
 			switch ai.Kind {
 			case typesEnumPrimitive:
 				ac.Data.(*Primitive).Output = ar.Data.(*Primitive).Output
 				ac.Data.(*Primitive).Check = ar.Data.(*Primitive).Check
 			}
 		}
-		switch {
-		case valueEquivalentValues(ac, ar, true):
-			continue
-		}
 		valPrincipalState.Creator[ii] = principalNamesMap["Attacker"]
 		valPrincipalState.Sender[ii] = principalNamesMap["Attacker"]
 		valPrincipalState.Mutated[ii] = true
@@ -167,6 +176,10 @@ func verifyActiveMutatePrincipalState(
 		if ii < earliestMutation {
 			earliestMutation = ii
 		}
+		switch {
+		case valueEquivalentValues(ac, ar, true):
+			continue
+		}
 		isWorthwhileMutation = true
 	}
 	if !isWorthwhileMutation {