Queries as preconditions for messages (experim.)

Imagine that we want to check, in the following model, if Alice will
only send some message to Alice if it has first authenticated it from
Bob:

```
attacker[active]

principal Bob[
    knows private psk
    generates m
    e = ENC(psk, m)
    h = MAC(psk, e)
]

Bob -> Alice: e, h

principal Alice[
    knows private psk
    _ = ASSERT(MAC(psk, e), h)?
    m2 = DEC(psk, e)
]

Alice -> Carol: [m2]

principal Carol[]
```

This can now be accomplished using the following query:

```
queries[
    authentication? Bob -> Alice: e[
	precondition[Alice -> Carol: m2]
    ]
]
```

The above query essentially expresses: "The event of Carol receiving m2 from
Alice shall only occur if Alice has previously received and
authenticated an encryption of m2 as coming from Bob."

This new syntax allows us to obtain some insight on the communication of
m2 based on the result of other queries, and to also link the
authentication of that communication on the authentication of other
values, which can be important when m2 is being communicated as a
guarded constant, which is the case in the above.

A new class of Verifpal language syntax is introduced here, called
"query options". Right now, "precondition" is the only query option, but
others may be added later, resulting in queries that look like this:

```
queries[
    confidentiality? x[
	precondition[Alice -> Carol: x2]
	precondition[Alice -> Carol: x3]
	someOtherOption[someOtherParameter]
    ]
]
```

cmd/verifpal/main_test.go

@@ -130,6 +130,10 @@ func TestMain(t *testing.T) {
 			model:       "signature.vp",
 			resultsCode: "c0a0a0",
 		},
+		{
+			model:       "precondition.vp",
+			resultsCode: "a1",
+		},
 	}
 	for _, v := range tests {
 		testModel(v, t)

examples/test/precondition.vp

+// SPDX-FileCopyrightText: © 2019-2020 Nadim Kobeissi <nadim@symbolic.software>
+// SPDX-License-Identifier: GPL-3.0-only
+
+attacker[active]
+
+principal Bob[
+	knows private psk
+	generates m
+	e = ENC(psk, m)
+	h = MAC(psk, e)
+]
+
+Bob -> Alice: e, h
+
+principal Alice[
+	knows private psk
+	_ = ASSERT(MAC(psk, e), h)
+	m2 = DEC(psk, e)
+]
+
+Alice -> Carol: m2
+
+principal Carol[]
+
+queries[
+	authentication? Bob -> Alice: e[
+		precondition[Alice -> Carol: m2]
+	]
+]
\ No newline at end of file

internal/verifpal/pretty.go

@@ -98,8 +98,24 @@ func prettyMessageColor(m string, t string, analysisCount int) {
 	}
 }
 
-func prettyVerifyResultSummary(mutated string, summary string, attack bool) string {
+func prettyVerifyResultSummary(mutated string, summary string, oResults []queryOptionResult, attack bool) string {
 	var mutatedIntro string
+	var optionsSummary string
+	for _, oResult := range oResults {
+		if !oResult.resolved {
+			continue
+		}
+		if len(optionsSummary) == 0 {
+			optionsSummary = fmt.Sprintf(
+				"%sFurthermore, the following options are contradicted:\n",
+				"           ",
+			)
+		}
+		optionsSummary = fmt.Sprintf(
+			"%s%s%s\n",
+			optionsSummary, "           - ", oResult.summary,
+		)
+	}
 	if !attack {
 		return summary
 	}
@@ -107,14 +123,15 @@ func prettyVerifyResultSummary(mutated string, summary string, attack bool) stri
 		mutatedIntro = "When the following values are controlled by the attacker:"
 	}
 	if colorOutputSupport() {
-		return fmt.Sprintf("%s%s\n           %s",
+		return fmt.Sprintf("%s%s\n           %s\n%s",
 			aurora.Italic(mutatedIntro).String(),
 			aurora.BrightYellow(mutated).Italic().String(),
 			aurora.BrightRed(summary).Italic().Bold().String(),
+			aurora.Magenta(optionsSummary).Italic().String(),
 		)
 	}
-	return fmt.Sprintf("%s%s\n           %s",
-		mutatedIntro, mutated, summary,
+	return fmt.Sprintf("%s%s\n           %s\n%s",
+		mutatedIntro, mutated, summary, optionsSummary,
 	)
 }
 

internal/verifpal/query.go

@@ -12,14 +12,10 @@ func queryStart(
 	query query, valKnowledgeMap knowledgeMap,
 	valPrincipalState principalState, valAttackerState attackerState,
 ) verifyResult {
-	result := verifyResult{
-		query:    query,
-		resolved: false,
-		summary:  "",
-	}
+	var result verifyResult
 	switch query.kind {
 	case "confidentiality":
-		result = queryConfidentiality(query, valPrincipalState, valAttackerState)
+		result = queryConfidentiality(query, valKnowledgeMap, valPrincipalState, valAttackerState)
 	case "authentication":
 		result = queryAuthentication(query, valKnowledgeMap, valPrincipalState, valAttackerState)
 	}
@@ -27,7 +23,7 @@ func queryStart(
 }
 
 func queryConfidentiality(
-	query query,
+	query query, valKnowledgeMap knowledgeMap,
 	valPrincipalState principalState, valAttackerState attackerState,
 ) verifyResult {
 	var mutated string
@@ -35,6 +31,7 @@ func queryConfidentiality(
 		query:    query,
 		resolved: false,
 		summary:  "",
+		options:  []queryOptionResult{},
 	}
 	ii := sanityEquivalentValueInValues(
 		sanityResolveConstant(query.constant, valPrincipalState),
@@ -58,12 +55,14 @@ func queryConfidentiality(
 		"%s is obtained by the attacker as %s",
 		prettyConstant(query.constant),
 		prettyValue(valAttackerState.known[ii]),
-	), true)
+	), result.options, true)
 	result = verifyResult{
 		query:    query,
 		resolved: true,
 		summary:  summary,
+		options:  []queryOptionResult{},
 	}
+	result = queryPrecondition(result, valKnowledgeMap, valPrincipalState)
 	written := verifyResultsPutWrite(result)
 	if written {
 		prettyMessage(fmt.Sprintf(
@@ -84,6 +83,7 @@ func queryAuthentication(
 		query:    query,
 		resolved: false,
 		summary:  "",
+		options:  []queryOptionResult{},
 	}
 	if query.message.recipient != valPrincipalState.name {
 		return result
@@ -140,39 +140,43 @@ func queryAuthentication(
 			}
 		}
 		if passes[f] && (query.message.sender != sender) {
-			summary := prettyVerifyResultSummary(mutated, fmt.Sprintf(
-				"%s, sent by %s and not by %s and resolving to %s, is successfully used in "+
-					"primitive %s in %s's state.",
-				prettyConstant(c), sender, query.message.sender,
-				prettyValue(cc), prettyValue(b), query.message.recipient,
-			), true)
 			result = verifyResult{
 				query:    query,
 				resolved: true,
-				summary:  summary,
+				summary:  "",
+				options:  []queryOptionResult{},
 			}
+			result = queryPrecondition(result, valKnowledgeMap, valPrincipalState)
+			result.summary = prettyVerifyResultSummary(mutated, fmt.Sprintf(
+				"%s, sent by %s and not by %s and resolving to %s,"+
+					" is successfully used in primitive %s in %s's state.",
+				prettyConstant(c), sender, query.message.sender,
+				prettyValue(cc), prettyValue(b), query.message.recipient,
+			), result.options, true)
 			written := verifyResultsPutWrite(result)
 			if written {
 				prettyMessage(fmt.Sprintf(
-					"%s: %s", prettyQuery(query), summary,
+					"%s: %s", prettyQuery(query), result.summary,
 				), "result", true)
 			}
 			return result
 		} else if forcedPasses[f] {
-			summary := prettyVerifyResultSummary(mutated, fmt.Sprintf(
-				"%s, sent by %s and resolving to %s, is successfully used in primitive %s in "+
-					"%s's state, despite it being vulnerable to tampering by Attacker.",
-				prettyConstant(c), sender, prettyValue(cc), prettyValue(b), query.message.recipient,
-			), true)
 			result = verifyResult{
 				query:    query,
 				resolved: true,
-				summary:  summary,
+				summary:  "",
+				options:  []queryOptionResult{},
 			}
+			result = queryPrecondition(result, valKnowledgeMap, valPrincipalState)
+			result.summary = prettyVerifyResultSummary(mutated, fmt.Sprintf(
+				"%s, sent by %s and resolving to %s, is successfully used in primitive %s in "+
+					"%s's state, despite it being vulnerable to tampering by Attacker.",
+				prettyConstant(c), sender, prettyValue(cc), prettyValue(b), query.message.recipient,
+			), result.options, true)
 			written := verifyResultsPutWrite(result)
 			if written {
 				prettyMessage(fmt.Sprintf(
-					"%s: %s", prettyQuery(query), summary,
+					"%s: %s", prettyQuery(query), result.summary,
 				), "result", true)
 			}
 			return result
@@ -180,3 +184,46 @@ func queryAuthentication(
 	}
 	return result
 }
+
+func queryPrecondition(
+	result verifyResult,
+	valKnowledgeMap knowledgeMap, valPrincipalState principalState,
+) verifyResult {
+	if !result.resolved {
+		return result
+	}
+	for _, option := range result.query.options {
+		oResult := queryOptionResult{
+			option:   option,
+			resolved: false,
+			summary:  "",
+		}
+		var sender string
+		recipientKnows := false
+		i := sanityGetPrincipalStateIndexFromConstant(
+			valPrincipalState, option.message.constants[0],
+		)
+		if i < 0 {
+			result.options = append(result.options, oResult)
+			continue
+		}
+		for _, m := range valKnowledgeMap.knownBy[i] {
+			if s, ok := m[option.message.recipient]; ok {
+				sender = s
+				recipientKnows = true
+				break
+			}
+		}
+		if sender == option.message.sender && recipientKnows {
+			oResult.resolved = true
+			oResult.summary = fmt.Sprintf(
+				"%s sends %s to %s despite the query being contradicted.",
+				option.message.sender,
+				prettyConstant(option.message.constants[0]),
+				option.message.recipient,
+			)
+		}
+		result.options = append(result.options, oResult)
+	}
+	return result
+}

internal/verifpal/types.go

@@ -15,6 +15,7 @@ type verifyResult struct {
 	query    query
 	resolved bool
 	summary  string
+	options  []queryOptionResult
 }
 
 type block struct {
@@ -51,6 +52,12 @@ type queryOption struct {
 	message message
 }
 
+type queryOptionResult struct {
+	option   queryOption
+	resolved bool
+	summary  string
+}
+
 type expression struct {
 	kind      string
 	qualifier string

internal/verifpal/verifyresults.go

@@ -20,6 +20,7 @@ func verifyResultsInit(m Model) bool {
 			query:    q,
 			resolved: false,
 			summary:  "",
+			options:  []queryOptionResult{},
 		}
 	}
 	verifyResultsFileNameShared = m.fileName