Merge remote-tracking branch 'upstream/develop' into develop

.gitignore

@@ -32,3 +32,5 @@ unit
 client_session_key.aes
 
 .DS_Store
+tags
+stack.yaml.lock

Makefile

@@ -349,58 +349,60 @@ regression-case-studies:	$(REGRESSION_TARGETS) $(SEQDFS_TARGETS)
 # FAST <=> processing time less than 10sec on Robert's current computer (per file)
 
 SAPIC_CASE_STUDIES_FAST=basic/no-replication.spthy basic/replication.spthy basic/channels1.spthy basic/channels2.spthy basic/channels3.spthy  basic/design-choices.spthy basic/exclusive-secrets.spthy basic/reliable-channel.spthy \
+basic/running-example.spthy \
+basic/operator-precedence-1.spthy basic/operator-precedence-2.spthy basic/operator-precedence-3.spthy basic/operator-precedence-4.spthy basic/operator-precedence-5.spthy \
 feature-let-bindings/let-blocks2.spthy feature-let-bindings/let-blocks3.spthy feature-let-bindings/match_new.spthy \
 statVerifLeftRight/stateverif_left_right.spthy \
 MoedersheimWebService/set-abstr.spthy MoedersheimWebService/set-abstr-lookup.spthy \
 fairexchange-mini/mini10.spthy fairexchange-mini/mini2.spthy fairexchange-mini/mini4.spthy fairexchange-mini/mini6.spthy fairexchange-mini/mini8.spthy fairexchange-mini/ndc-nested-2.spthy fairexchange-mini/ndc-nested-4.spthy fairexchange-mini/ndc-nested.spthy fairexchange-mini/mini1.spthy fairexchange-mini/mini3.spthy fairexchange-mini/mini5.spthy fairexchange-mini/mini7.spthy fairexchange-mini/mini9.spthy fairexchange-mini/ndc-nested-3.spthy fairexchange-mini/ndc-nested-5.spthy fairexchange-mini/ndc-two-replications.spthy\
 SCADA/opc_ua_secure_conversation.spthy \
 feature-xor/CH07.spthy feature-xor/CRxor.spthy feature-xor/KCL07.spthy \
 feature-secret-channel/secret-channel.spthy \
-GJM-contract/contract.spthy
-# not working because of missing support for predicates
-# basic/running-example.spthy feature-let-bindings/let-blocks.spthy 
-# encWrapDecUnwrap/encwrapdecunwrap.spthy NOTE: might be not working for other reasons as well, it was commented out investigate
-# Yubikey/Yubikey.spthy NOTE commented out previously need to verify
-# PKCS11/pkcs11-templates.spthy PKCS11/pkcs11-dynamic-policy.spthy \ NOTE commented out previously need to verify
-# feature-predicates/decwrap_destr.spthy feature-predicates/simple_example.spthy \
-# location stuff: not tested so far
-# feature-locations/AC.spthy feature-locations/AKE.spthy feature-locations/licensing.spthy \
-# feature-locations/SOC.spthy  -> commented out before
-# examples/sapic/feature-locations/OTP.sapic examples/sapic/feature-locations/AC.sapic examples/sapic/feature-locations/AC_counter_with_attack.sapic examples/sapic/feature-locations/AC_sid_with_attack.sapic -> not in Makefile before
-# pkcs11-example were previously commented out because they took so long, but should check if they can be completed.
-# examples/sapic/PKCS11/pkcs11-templates.sapic
-# examples/sapic/PKCS11/pkcs11-dynamic-policy.sapic
+GJM-contract/contract.spthy \
+feature-predicates/decwrap-destr-manual.spthy feature-predicates/decwrap-destr-restrict.spthy feature-predicates/decwrap-destr-restrict-variant.spthy feature-predicates/pub.spthy feature-predicates/simple_example.spthy feature-predicates/binding.spthy \
+feature-predicates/binding.spthy \
+feature-let-bindings/let-blocks.spthy \
+feature-locations/AC.spthy \
+feature-locations/AKE.spthy  \
+feature-locations/licensing.spthy \
+feature-locations/SOC.spthy \
+feature-locations/OTP.spthy \
+feature-locations/AC_counter_with_attack.spthy \
+feature-locations/AC_sid_with_attack.spthy \
+feature-ass-immediate/test-all.spthy 
+
+# SLOW <=> processing time more than 10sec on Robert's current computer, but less than a day
+SAPIC_CASE_STUDIES_SLOW= encWrapDecUnwrap/encwrapdecunwrap-nolocks.spthy \
+NSL/nsl-no_as-untagged.spthy \
+Yubikey/Yubikey.spthy \
+encWrapDecUnwrap/encwrapdecunwrap.spthy
+
+# SUPER SLOW <=> processing time more than a day or take's more memory than Robert's computer can take
+SAPIC_CASE_STUDIES_SUPER_SLOW= fairexchange-km/km.spthy \
+fairexchange-asw/aswAB.spthy \
+examples/sapic/fairexchange-asw/asw-mod-weak-locks.spthy \
+examples/sapic/fairexchange-asw/aswAB-mod.spthy \
+fairexchange-gjm/gjm-locks-fakepcsbranch.spthy \
+fairexchange-gjm/gjm-locks-unfairness-A.spthy
+
+# The following case studies are in the repository, but cannot be proven automatically.
+# PKCS11/pkcs11-templates.spthy 
+# # heavy use of manual lemmas, not part of regresstion tests
+#
+# PKCS11/pkcs11-dynamic-policy.spthy \ 
+# # not working 
 #
-# exceptional cases, that are left out on purpose, with explanations:
-# xor/NSLPK3xor.spthy: attack finding relies on sources lemma which is untrue. it is acceptable for this model, 
-# 		because the attacks found despite an incorrect sources lemma
-# 		are correct by definition, but negating it would defeat its
-# 		purpose, and removing it would inhibit the attack finding. 
+# feature-xor/NSLPK3xor.spthy \
+# # attack finding relies on sources lemma which is untrue. it is acceptable for
+# # this model, because the attacks found despite an incorrect sources lemma are
+# # correct by definition, but negating it would defeat its purpose, and removing
+# # it would inhibit the attack finding. 
 #
-# missing (but also before): fairexchange stuff...-> check how long they take on fast machines
-# examples/sapic/fairexchange-km/km.sapic
-# examples/sapic/fairexchange-km/km-with-comments.sapic
-# examples/sapic/fairexchange-asw/aswAB-mod-weak-A.sapic
-# examples/sapic/fairexchange-asw/asw-mod-weak-locks.sapic
-# examples/sapic/fairexchange-asw/aswAB-mod-weak-B.sapic
-# examples/sapic/fairexchange-asw/aswAB.sapic
-# examples/sapic/fairexchange-asw/aswAB-mod.sapic
-# examples/sapic/fairexchange-gjm/gjm-locks-magic.sapic
-# examples/sapic/fairexchange-gjm/gjm-locks-fakepcsbranch-B.sapic
-# examples/sapic/fairexchange-gjm/gjm-locks-fakepcsbranch.sapic
-# examples/sapic/fairexchange-gjm/gjm-locks-unfairness-A.sapic
-# examples/sapic/fairexchange-gjm/gjm.sapic
-# examples/sapic/fairexchange-gjm/gjm-locks.sapic#
-
-# envelope examples (this example was never completed and is for reference only)
-# examples/sapic/envelope/envelope.sapic
-# examples/sapic/envelope/envelope_simpler.sapic
-# examples/sapic/envelope/envelope_allowsattack.sapic
+# envelope/envelope.spthy envelope/envelope_simpler.spthy envelope/envelope_allowsattack.spthy \ 
+# # these examples were never completed and are here for reference only
+
+# not working because of missing support for locations
 
-# SLOW <=> processing time more than 10sec on Robert's current computer, but less than a day
-SAPIC_CASE_STUDIES_SLOW=encWrapDecUnwrap/encwrapdecunwrap-nolocks.spthy \
-NSL/nsl-no_as-untagged.spthy 
-SAPIC_CASE_STUDIES_SUPER_SLOW=fairexchange-asw/aswAB.spthy
 
 SAPIC_CS_TARGETS_FAST=$(subst .spthy,_analyzed.spthy,$(addprefix case-studies/sapic/,$(SAPIC_CASE_STUDIES_FAST)))
 SAPIC_CS_TARGETS_SLOW=$(subst .spthy,_analyzed.spthy,$(addprefix case-studies/sapic/,$(SAPIC_CASE_STUDIES_SLOW)))
@@ -414,7 +416,7 @@ sapic-case-studies:	$(SAPIC_CS_TARGETS_FAST) $(SAPIC_CS_TARGETS_SLOW) # used for
 	grep "verified\|falsified\|processing time" $^
 sapic-case-studies-fast:	$(SAPIC_CS_TARGETS_FAST) # used for quick checks during development
 	grep "verified\|falsified\|processing time" $^
-sapic-case-studies-superslow:	$(SAPIC_CS_TARGETS_SUPERSLOW) # used to heat in winter
+sapic-case-studies-superslow:	$(SAPIC_CS_TARGETS_SUPER_SLOW) # used to heat in winter
 	grep "verified\|falsified\|processing time" $^
 
 ## All case studies