Add equivalence query support

CHANGELOG.md

@@ -5,33 +5,46 @@
 
 # Change Log
 
+## 1.0.9
+
+- Add support for `equivalence` queries.
+
 ## 1.0.8
+
 - Fix a typo.
 
 ## 1.0.7
+
 - Add support for the new `BLIND` and `UNBLIND` primitives.
 
 ## 1.0.6
+
 - Fix diagrams being hard to read with certain VSCode themes.
 
 ## 1.0.5
+
 - Diagrams now display properly in Visual Studio Code editors using dark themes.
 
 ## 1.0.4
+
 - Correctly handle errors when user attempts to analyze or visualize an invalid model (due to syntax errors or similar).
 
 ## 1.0.3
+
 - Fixed a typo.
 
 ## 1.0.2
+
 - Fix a bug that prevented diagram visualizations for working on Windows.
 - Removed a message that incessantly kept popping up asking the user to set `verifpal.path`.
 
 ## 1.0.1
+
 - Move beyond deprecated VSCode extension APIs.
 - Improve documentation.
 
 ## 1.0.0
+
 - Add live analysis support (requires Verifpal 0.13.0 or higher).
 - Add formatting support (requires Verifpal 0.13.0 or higher).
 - Add hover information support (requires Verifpal 0.13.0 or higher).
@@ -39,37 +52,49 @@
 - Add diagram generation support (requires Verifpal 0.13.0 or higher).
 
 ## 0.0.12
+
 - Add `freshness` and `unlinkability` query keywords.
 
 ## 0.0.11
+
 - `SPLIT` keyword incorrectly added as `JOIN`.
 
 ## 0.0.10
+
 - Add `CONCAT` and `JOIN` keywords.
 
 ## 0.0.9
+
 - Add `RINGSIGN` and `RINGSIGNVERIF` keywords.
 
 ## 0.0.8
+
 - Add `leaks` declaration keyword.
 
 ## 0.0.7
+
 - Add `phase` block keyword.
 
 ## 0.0.6
+
 - Added `PW_HASH` and `password` keywords.
 
 ## 0.0.5
+
 - Added `SHAMIR_SPLIT` and `SHAMIR_JOIN` keywords.
 
 ## 0.0.4
+
 - Added `PKE_ENC` and `PKE_DEC` keywords.
 
 ## 0.0.3
+
 - Added `nil` and `_` keywords.
 
 ## 0.0.2
+
 - Updated syntax highlighting to match the renaming of `HMACVERIF` to `ASSERT` and `HMAC` to `MAC`.
 
 ## 0.0.1
+
 - Initial release.

package.json

@@ -81,12 +81,12 @@
 		"compile": "tsc -watch -p ./"
 	},
 	"devDependencies": {
-		"@types/vscode": "^1.44.0",
 		"@types/node": "latest",
-		"typescript": "latest",
-		"eslint": "latest",
+		"@types/vscode": "^1.44.0",
 		"@typescript-eslint/eslint-plugin": "latest",
-		"@typescript-eslint/parser": "latest"
+		"@typescript-eslint/parser": "latest",
+		"eslint": "latest",
+		"typescript": "latest"
 	},
 	"dependencies": {
 		"cross-spawn": "latest"

src/AnalysisProvider.ts

@@ -112,6 +112,11 @@ export default class AnalysisProvider {
 							constantNames.push(verifyResults[i].Query.Constants[ii].Name);
 						}
 						break;
+					case "equivalence":
+						for (let ii = 0; ii < verifyResults[i].Query.Constants.length; ii++) {
+							constantNames.push(verifyResults[i].Query.Constants[ii].Name);
+						}
+						break;
 					}
 					let formattedSummary = verifyResults[i].Summary.replace(/\[(\d|;)+m/gm, "");
 					let p = {

src/VerifpalLib.ts

@@ -250,6 +250,10 @@ export default class VerifpalLib {
 			"unlinkability": {
 				eg: "unlinkability? a, b, c",
 				help: "Checks whether all given values satisfy freshness. If they do, checks whether the attacker can determine them as being the output of the same primitive or as otherwise having a common source. If any of these checks fail, the query fails.",
+			},
+			"equivalence": {
+				eg: "equivalence? ss_a, ss_b",
+				help: "Checks whether any protocol scenario can be derived such that the given values are not equivalent to one another. This query could be useful for checking if all parties derived the same shared secret, for example."
 			}
 		};
 		if (({}).hasOwnProperty.call(queries, queryName.toLowerCase())) {

syntax/verifpal.iro

@@ -121,7 +121,7 @@ contexts [] {
          styles []       = .punctuation;
       }
       : pattern {
-         regex          \= (confidentiality\?|authentication\?|freshness\?|unlinkability\?)
+         regex          \= (confidentiality\?|authentication\?|freshness\?|unlinkability\?equivalence\?)
          styles []       = .keyword;
       }
       : pattern {
@@ -142,7 +142,7 @@ contexts [] {
          : include "main";
       }
       : inline_push {
-         regex          \= (((confidentiality)|(authentication)|(freshness)|(unlinkability))\?)
+         regex          \= (((confidentiality)|(authentication)|(freshness)|(unlinkability)|(equivalence))\?)
          styles []       = .keyword;
          : pop {  
             regex       \= (\s\-\>\s)

syntax/verifpal.tmLanguage

@@ -208,7 +208,7 @@
         </dict>
         <dict>
           <key>match</key>
-          <string>(confidentiality\?|authentication\?|freshness\?|unlinkability\?)</string>
+          <string>(confidentiality\?|authentication\?|freshness\?|unlinkability\?|equivalence\?)</string>
           <key>name</key>
           <string>markup.italic.verifpal</string>
         </dict>
@@ -249,7 +249,7 @@
         </dict>
         <dict>
           <key>begin</key>
-          <string>(((confidentiality)|(authentication)|(freshness)|(unlinkability))\?)</string>
+          <string>(((confidentiality)|(authentication)|(freshness)|(unlinkability)|(equivalence))\?)</string>
           <key>beginCaptures</key>
           <dict>
             <key>1</key>