Commit 205ae77b authored by Nadim Kobeissi's avatar Nadim Kobeissi 💾
Browse files

Add more sanity checks

parent 0d24442c
Pipeline #817 passed with stages
in 1 minute and 20 seconds
......@@ -229,7 +229,7 @@ func prettyExpression(expression Expression) string {
func prettyMessage(block Block) string {
output := fmt.Sprintf(
"%s -> %s: %s\n\n",
"%s -> %s: %s",
principalGetNameFromID(block.Message.Sender),
principalGetNameFromID(block.Message.Recipient),
prettyConstants(block.Message.Constants),
......@@ -261,7 +261,7 @@ func PrettyModel(m Model) (string, error) {
case "principal":
output = output + prettyPrincipal(block)
case "message":
output = output + prettyMessage(block)
output = output + prettyMessage(block) + "\n\n"
case "phase":
output = output + prettyPhase(block)
}
......@@ -302,7 +302,7 @@ func PrettyDiagram(m Model) (string, error) {
}
output = fmt.Sprintf("%s\n", output)
case "message":
output = output + prettyMessage(block)
output = output + prettyMessage(block) + "\n"
case "phase":
output = fmt.Sprintf(
"%sNote left of %s:phase %d\n",
......
......@@ -226,13 +226,11 @@ func sanityQueriesAuthentication(query Query, valKnowledgeMap *KnowledgeMap) err
prettyQuery(query),
)
}
if query.Message.Sender == query.Message.Recipient {
return fmt.Errorf(
"authentication query (%s) has identical sender and recipient",
prettyQuery(query),
)
}
c := query.Message.Constants[0]
err := sanityQueriesCheckMessagePrincipals(query.Message)
if err != nil {
return err
}
return sanityQueriesCheckKnown(query, query.Message, c, valKnowledgeMap)
}
......@@ -255,13 +253,18 @@ func sanityQueriesUnlinkability(query Query, valKnowledgeMap *KnowledgeMap) erro
prettyQuery(query),
)
}
for _, c := range query.Constants {
i := valueGetKnowledgeMapIndexFromConstant(valKnowledgeMap, c)
if i < 0 {
for i := 0; i < len(query.Constants); i++ {
ii := valueGetKnowledgeMapIndexFromConstant(valKnowledgeMap, query.Constants[i])
if ii < 0 {
return fmt.Errorf(
"unlinkability query (%s) refers to unknown constant (%s)",
prettyQuery(query),
prettyConstant(c),
prettyQuery(query), prettyConstant(query.Constants[i]),
)
}
if valueEquivalentConstantInConstants(query.Constants[i], query.Constants[:i]) >= 0 {
return fmt.Errorf(
"unlinkability query (%s) refers to same constant more than once (%s)",
prettyQuery(query), prettyConstant(query.Constants[i]),
)
}
}
......@@ -279,6 +282,10 @@ func sanityQueryOptions(query Query, valKnowledgeMap *KnowledgeMap) error {
)
}
c := option.Message.Constants[0]
err := sanityQueriesCheckMessagePrincipals(option.Message)
if err != nil {
return err
}
return sanityQueriesCheckKnown(query, option.Message, c, valKnowledgeMap)
default:
return fmt.Errorf("invalid query option kind")
......@@ -287,6 +294,16 @@ func sanityQueryOptions(query Query, valKnowledgeMap *KnowledgeMap) error {
return nil
}
func sanityQueriesCheckMessagePrincipals(message Message) error {
if message.Sender == message.Recipient {
return fmt.Errorf(
"query with message (%s) has identical sender and recipient",
prettyMessage(Block{Kind: "message", Message: message}),
)
}
return nil
}
func sanityQueriesCheckKnown(query Query, m Message, c *Constant, valKnowledgeMap *KnowledgeMap) error {
senderKnows := false
recipientKnows := false
......
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