Renaming SAPIC options for consistency. (tamarin-prover#526)

Co-authored-by: Robert Künnemann <robert.kuennemann@cispa.saarland>
yavivanov · Mar 8, 2023 · ef1c24a · ef1c24a
1 parent 958f8b1
commit ef1c24a
Show file tree

Hide file tree

Showing 12 changed files with 17 additions and 16 deletions.
diff --git a/etc/docker/res/proverif-tamarin-diff b/etc/docker/res/proverif-tamarin-diff
@@ -2,4 +2,4 @@
 
 set -x # print what we do
 temp=$(mktemp -d)/$(basename "$1")
-tamarin-prover "$1" --diff -m=proverifequiv > "$temp.pv"; proverif "$temp.pv"
+tamarin-prover "$1" -m=proverifequiv > "$temp.pv"; proverif "$temp.pv"
diff --git a/examples/sapic/export/5G_AKA/5G_AKA.spthy b/examples/sapic/export/5G_AKA/5G_AKA.spthy
@@ -219,8 +219,8 @@ functions:
 	KDF/2,	 // KDF		 --> K_ausf, K_seaf, XRES*
 	SHA256/2 // KDF		 --> HXRES*
 
-options: enableStateOpt,
-asynchronous-channels, compress-events,
+options: translation-state-optimisation,
+translation-asynchronous-channels, translation-compress-events,
 translation-allow-pattern-lookups
 
 

diff --git a/examples/sapic/export/ExistingSapicModels/AC.spthy b/examples/sapic/export/ExistingSapicModels/AC.spthy
@@ -13,7 +13,7 @@ builtins: dest-pairing, locations-report
 functions: prog/3,list/2
 heuristic: S
 
-options: enableStateOpt
+options: translation-state-optimisation
 
 predicates:
 Report(x,y) <=> not  (y= 'loc')

diff --git a/examples/sapic/export/ExistingSapicModels/AC_counter_with_attack.spthy b/examples/sapic/export/ExistingSapicModels/AC_counter_with_attack.spthy
@@ -10,7 +10,7 @@ functions: prog/3,null/0,succ/1,list/2
 
 heuristic:S
 
-options: enableStateOpt
+options: translation-state-optimisation
 
 predicates:
 Report(x,y) <=> not  (y= 'l')

diff --git a/examples/sapic/export/ExistingSapicModels/AC_sid_with_attack.spthy b/examples/sapic/export/ExistingSapicModels/AC_sid_with_attack.spthy
@@ -7,7 +7,7 @@ theory AC_sid
 
 begin
 
-//options: enableStateOpt
+//options: translation-state-optimisation
 
 builtins: dest-pairing, locations-report
 

diff --git a/examples/sapic/export/States/canauth.spthy b/examples/sapic/export/States/canauth.spthy
@@ -12,7 +12,7 @@ section{* CANauth protocol *}
 */
 builtins: dest-pairing, multiset
 
-options: enableStateOpt
+options: translation-state-optimisation
 
 functions: hmac(bitstring,bitstring):bitstring
 

diff --git a/examples/sapic/export/States/secure-device.spthy b/examples/sapic/export/States/secure-device.spthy
@@ -11,7 +11,7 @@ theory StatVerif_Security_Device begin
 
 builtins: dest-pairing, dest-asymmetric-encryption
 
-//options: enableStateOpt
+//options: translation-state-optimisation
 
 let Device=(
 	out(pk(~sk))

diff --git a/examples/sapic/fast/Yubikey/Yubikey.spthy b/examples/sapic/fast/Yubikey/Yubikey.spthy
@@ -10,7 +10,7 @@ section{* The Yubikey-Protocol *}
  */
 
 builtins: symmetric-encryption, multiset
-options: enableStateOpt
+options: translation-state-optimisation
 
 let Yubikey(L_pid,YL_pid,SL_pid,secretid,k)=
  !(( //Plug

diff --git a/examples/sapic/fast/feature-locations/AC.spthy b/examples/sapic/fast/feature-locations/AC.spthy
@@ -13,7 +13,7 @@ builtins: locations-report
 functions: prog/3,list/2
 heuristic: S
 
-options: enableStateOpt
+options: translation-state-optimisation
 
 predicates:
 Report(x,y) <=> not  (y= 'loc')

diff --git a/examples/sapic/fast/feature-locations/AC_counter_with_attack.spthy b/examples/sapic/fast/feature-locations/AC_counter_with_attack.spthy
@@ -10,7 +10,7 @@ functions: prog/3,null/0,succ/1,list/2
 
 heuristic:S
 
-options: enableStateOpt
+options: translation-state-optimisation
 
 predicates:
 Report(x,y) <=> not  (y= 'l')

diff --git a/examples/sapic/slow/feature-locations/AC_sid_with_attack.spthy b/examples/sapic/slow/feature-locations/AC_sid_with_attack.spthy
@@ -7,7 +7,7 @@ theory AC_sid
 
 begin
 
-//options: enableStateOpt
+//options: translation-state-optimisation
 
 builtins: locations-report
 

diff --git a/lib/theory/src/Theory/Text/Parser/Signature.hs b/lib/theory/src/Theory/Text/Parser/Signature.hs
@@ -183,11 +183,12 @@ options thy0 =do
     setOption' thy Nothing  = thy
     setOption' thy (Just l) = setOption l thy
     builtinTheory = asum
-      [  try (symbol "translation-progress") Data.Functor.$> Just transProgress
+      [  try 
+         (symbol "translation-progress") Data.Functor.$> Just transProgress
         , symbol "translation-allow-pattern-lookups" Data.Functor.$> Just transAllowPatternMatchinginLookup
-        , symbol "enableStateOpt" Data.Functor.$> Just stateChannelOpt
-        , symbol "asynchronous-channels" Data.Functor.$> Just asynchronousChannels
-        , symbol "compress-events" Data.Functor.$> Just compressEvents
+        , symbol "translation-state-optimisation" Data.Functor.$> Just stateChannelOpt
+        , symbol "translation-asynchronous-channels" Data.Functor.$> Just asynchronousChannels
+        , symbol "translation-compress-events" Data.Functor.$> Just compressEvents
       ]
 
 predicate :: Parser Predicate