readme

process_complete_mininal_tests/__tamarin__/myoracle

+#!/usr/bin/env python3
+from __future__ import print_function
+import sys
+lines = sys.stdin.readlines()
+l1 = []
+l2 = []
+
+lemma = sys.argv[1]
+for line in lines:
+  num = line.split(':')[0]
+  if (lemma == "Agreement_InitHello" or "Agreement_Transport_itor" or "Secrecy_R_SK_ItoR_PFS" or "Secrecy_R_SK_RtoI_PFS" or "Secrecy_R_SK_ItoR" or "Secrecy_R_SK_RtoI" or "Agreement_Confirm" or "Secrecy_RK6" or "Secrecy_RK6_PFS"):
+      if "splitEqs(0)" in line:
+        l1.append(num)
+      else:
+        l2.append(num)
+  else:
+    exit(0)
+ranked = l1 + l2
+for i in ranked:
+  print(i)

process_complete_mininal_tests/run_evaluate-pv.sh

 #!/bin/sh
 
-eval $(opam --safe env)
+eval $(opam env)
 
 JOBS=6
 
@@ -14,4 +14,4 @@ cd ../secrecy_rsk6_pfs
 
 echo "Evaluate ProVerif queries for isk6 pfs"
 
-time -p -f "%E" parallel --jobs $JOBS < wireguard_command
\ No newline at end of file
+time -p -f "%E" parallel --jobs $JOBS < wireguard_command