Commit 13fbcab9 authored by Nadim Kobeissi's avatar Nadim Kobeissi 💎

Improved attack traces/summaries output

parent 52cf2e7f
Pipeline #622 failed with stages
in 18 seconds
......@@ -214,7 +214,11 @@ func infoOutputText(revealed Value) string {
}
}
func infoQueryMutatedValues(valKnowledgeMap KnowledgeMap, valPrincipalState PrincipalState) string {
func infoQueryMutatedValues(
valKnowledgeMap KnowledgeMap, valPrincipalState PrincipalState,
valAttackerState AttackerState, targetValue Value,
) string {
mutated := []Value{}
mutatedInfo := ""
for i, a := range valPrincipalState.BeforeRewrite {
if valueEquivalentValues(a, valKnowledgeMap.Assigned[i], false) {
......@@ -222,34 +226,67 @@ func infoQueryMutatedValues(valKnowledgeMap KnowledgeMap, valPrincipalState Prin
}
pc := prettyConstant(valPrincipalState.Constants[i])
pa := prettyValue(valPrincipalState.Assigned[i])
isTarget := valueEquivalentValues(targetValue, valPrincipalState.Assigned[i], false)
if !isTarget && valPrincipalState.Mutated[i] {
if valueEquivalentValueInValues(valPrincipalState.Assigned[i], mutated) < 0 {
mutated = append(mutated, valPrincipalState.Assigned[i])
}
}
pn := make([]string, 4)
if colorOutputSupport() {
if valPrincipalState.Mutated[i] {
mutatedInfo = fmt.Sprintf("%s\n %s%s%s %s",
mutatedInfo,
aurora.BrightYellow(pc).Italic().Underline().String(),
aurora.BrightYellow(" → ").Italic().Underline().String(),
aurora.BrightYellow(pa).Italic().Underline().String(),
aurora.Red("(mutated by attacker)").Italic().String(),
)
} else {
mutatedInfo = fmt.Sprintf("%s\n %s%s%s",
mutatedInfo,
aurora.BrightYellow(pc).Italic().String(),
aurora.BrightYellow(" → ").Italic().String(),
aurora.BrightYellow(pa).Italic().String(),
)
pn[0] = aurora.BrightYellow(pc).Italic().String()
pn[1] = aurora.BrightYellow(" → ").Italic().String()
pn[2] = aurora.BrightYellow(pa).Italic().String()
pn[3] = ""
if isTarget && !valPrincipalState.Mutated[i] {
pn[0] = aurora.BrightYellow(pc).Italic().Underline().String()
pn[1] = aurora.BrightYellow(" → ").Italic().Underline().String()
pn[2] = aurora.BrightYellow(pa).Italic().Underline().String()
pn[3] = aurora.Red("← obtained by Attacker").Italic().String()
} else if valPrincipalState.Mutated[i] {
pn[3] = aurora.Red("← mutated by Attacker").Italic().String()
}
} else {
if valPrincipalState.Mutated[i] {
mutatedInfo = fmt.Sprintf("%s\n %s%s%s %s",
mutatedInfo, pc, " → ", pa, "(mutated by attacker)",
)
} else {
mutatedInfo = fmt.Sprintf("%s\n %s%s%s",
mutatedInfo, pc, " → ", pa,
)
pn[0] = pc
pn[1] = " → "
pn[2] = pa
pn[3] = ""
if isTarget && !valPrincipalState.Mutated[i] {
pn[3] = "← obtained by Attacker"
} else if valPrincipalState.Mutated[i] {
pn[3] = "← mutated by Attacker"
}
}
mutatedInfo = fmt.Sprintf("%s\n %s%s%s %s",
mutatedInfo, pn[0], pn[1], pn[2], pn[3],
)
}
for _, m := range mutated {
ai := valueEquivalentValueInValues(m, valAttackerState.Known)
if ai < 0 {
continue
}
mmInfo := infoQueryMutatedValues(valKnowledgeMap, valAttackerState.PrincipalState[ai], valAttackerState, m)
if len(mmInfo) == 0 {
continue
}
if colorOutputSupport() {
mutatedInfo = fmt.Sprintf(
"%s\n\n %s%s\n%s",
mutatedInfo,
aurora.Italic(prettyValue(m)).String(),
aurora.Italic(", used above, is obtained when, in a previous session:").String(),
mmInfo,
)
} else {
mutatedInfo = fmt.Sprintf(
"%s\n\n %s%s\n%s",
mutatedInfo,
prettyValue(m),
", used above, is obtained when, in a previous session:",
mmInfo,
)
}
}
return mutatedInfo
}
......@@ -17,7 +17,7 @@ func queryStart(
case "confidentiality":
queryConfidentiality(query, valKnowledgeMap, valPrincipalState, valAttackerState)
case "authentication":
queryAuthentication(query, valKnowledgeMap, valPrincipalState)
queryAuthentication(query, valKnowledgeMap, valPrincipalState, valAttackerState)
case "freshness":
_, err = queryFreshness(query, valKnowledgeMap, valPrincipalState, valAttackerState)
case "unlinkability":
......@@ -44,7 +44,9 @@ func queryConfidentiality(
if ii < 0 {
return result
}
mutatedInfo := infoQueryMutatedValues(valKnowledgeMap, valAttackerState.PrincipalState[ii])
mutatedInfo := infoQueryMutatedValues(
valKnowledgeMap, valAttackerState.PrincipalState[ii], valAttackerState, v,
)
result.Resolved = true
result.Summary = infoVerifyResultSummary(mutatedInfo, fmt.Sprintf(
"%s (%s) is obtained by Attacker.",
......@@ -62,7 +64,8 @@ func queryConfidentiality(
}
func queryAuthentication(
query Query, valKnowledgeMap KnowledgeMap, valPrincipalState PrincipalState,
query Query, valKnowledgeMap KnowledgeMap,
valPrincipalState PrincipalState, valAttackerState AttackerState,
) VerifyResult {
result := VerifyResult{
Query: query,
......@@ -81,10 +84,15 @@ func queryAuthentication(
continue
}
result.Resolved = true
mutatedInfo := infoQueryMutatedValues(valKnowledgeMap, valPrincipalState)
result = queryPrecondition(result, valPrincipalState)
a := valPrincipalState.Assigned[index]
b := valPrincipalState.BeforeRewrite[index]
return queryAuthenticationHandlePass(result, c, b, mutatedInfo, sender, valPrincipalState)
mutatedInfo := infoQueryMutatedValues(
valKnowledgeMap, valPrincipalState, valAttackerState, a,
)
result = queryPrecondition(result, valPrincipalState)
return queryAuthenticationHandlePass(
result, c, b, mutatedInfo, sender, valPrincipalState,
)
}
return result
}
......@@ -184,13 +192,16 @@ func queryFreshness(
if freshnessFound {
return result, nil
}
mutatedInfo := infoQueryMutatedValues(valKnowledgeMap, valPrincipalState)
resolved, _ := valueResolveConstant(query.Constants[0], valPrincipalState)
mutatedInfo := infoQueryMutatedValues(
valKnowledgeMap, valPrincipalState, valAttackerState, resolved,
)
result.Resolved = true
result.Summary = infoVerifyResultSummary(mutatedInfo, fmt.Sprintf(
"%s (%s) is not a fresh value. If used as a message, it could be replayed, leading to potential replay attacks.",
"%s (%s) is not a fresh value. If used as a message, %s",
prettyConstant(query.Constants[0]),
prettyValue(resolved),
"it could be replayed, leading to potential replay attacks.",
), result.Options)
result = queryPrecondition(result, valPrincipalState)
written := verifyResultsPutWrite(result)
......@@ -234,8 +245,10 @@ func queryUnlinkability(
}
}
if len(noFreshness) > 0 {
mutatedInfo := infoQueryMutatedValues(valKnowledgeMap, valPrincipalState)
resolved, _ := valueResolveConstant(noFreshness[0], valPrincipalState)
mutatedInfo := infoQueryMutatedValues(
valKnowledgeMap, valPrincipalState, valAttackerState, resolved,
)
result.Resolved = true
result.Summary = infoVerifyResultSummary(mutatedInfo, fmt.Sprintf(
"%s (%s) cannot be a suitable unlinkability candidate since it does not satisfy freshness.",
......@@ -276,7 +289,9 @@ func queryUnlinkability(
if !obtainable {
continue
}
mutatedInfo := infoQueryMutatedValues(valKnowledgeMap, valPrincipalState)
mutatedInfo := infoQueryMutatedValues(
valKnowledgeMap, valPrincipalState, valAttackerState, Value{},
)
result.Resolved = true
result.Summary = infoVerifyResultSummary(mutatedInfo, fmt.Sprintf(
"%s and %s %s (%s), %s.",
......
......@@ -46,7 +46,6 @@ func verifyModel(m Model) ([]VerifyResult, string, error) {
default:
return []VerifyResult{}, "", fmt.Errorf("invalid attacker (%s)", m.Attacker)
}
fmt.Fprint(os.Stdout, "\n\n")
return verifyEnd(m)
}
......@@ -154,6 +153,15 @@ func verifyGetResultsCode(valVerifyResults []VerifyResult) string {
func verifyEnd(m Model) ([]VerifyResult, string, error) {
var err error
valVerifyResults, fileName := verifyResultsGetRead()
completed := time.Now().Format("03:04:05 PM")
fmt.Fprint(os.Stdout, "\n\n")
InfoMessage(fmt.Sprintf(
"Verification completed for '%s' at %s.", fileName, completed,
), "verifpal", false)
InfoMessage(fmt.Sprintf(
"Summary of contradicted queries, if any, will follow.",
), "verifpal", false)
fmt.Fprint(os.Stdout, "\n")
for _, verifyResult := range valVerifyResults {
if verifyResult.Resolved {
InfoMessage(fmt.Sprintf(
......@@ -163,10 +171,6 @@ func verifyEnd(m Model) ([]VerifyResult, string, error) {
), "result", false)
}
}
completed := time.Now().Format("03:04:05 PM")
InfoMessage(fmt.Sprintf(
"Verification completed for '%s' at %s.", fileName, completed,
), "verifpal", false)
InfoMessage("Thank you for using Verifpal.", "verifpal", false)
resultsCode := verifyGetResultsCode(valVerifyResults)
if VerifHubScheduledShared {
......
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