diff --git a/spdl/SPORE/denning-sacco-lowe.spdl b/spdl/SPORE/denning-sacco-lowe.spdl index bb0e576..b5d0608 100644 --- a/spdl/SPORE/denning-sacco-lowe.spdl +++ b/spdl/SPORE/denning-sacco-lowe.spdl @@ -4,10 +4,6 @@ # http://www.lsv.ens-cachan.fr/spore/denningSaccoLowe.html # # Note: -# This protocol uses a ticket so scyther will only be able to verify -# the protocol using the ARACHNE engine (-a) -# -# Note: # According to SPORE there are no attacks on this protocol, scyther # finds one however. This has to be investigated further. diff --git a/spdl/SPORE/denning-sacco.spdl b/spdl/SPORE/denning-sacco.spdl index 3fd1d94..c725048 100644 --- a/spdl/SPORE/denning-sacco.spdl +++ b/spdl/SPORE/denning-sacco.spdl @@ -3,10 +3,6 @@ # Modelled after the description in the SPORE library # http://www.lsv.ens-cachan.fr/spore/denningSacco.html # -# Note: -# This protocol uses a ticket so scyther will only be able to verify -# the protocol using the ARACHNE engine (-a) -# usertype Key; usertype SessionKey; diff --git a/spdl/SPORE/kaochow-v2.spdl b/spdl/SPORE/kaochow-v2.spdl index 450a60f..731fe3a 100644 --- a/spdl/SPORE/kaochow-v2.spdl +++ b/spdl/SPORE/kaochow-v2.spdl @@ -3,10 +3,6 @@ # Modelled after the description in the SPORE library # http://www.lsv.ens-cachan.fr/spore/kaoChow2.html # -# Note: -# This protocol uses a ticket so scyther will only be able to verify -# the protocol using the ARACHNE engine (-a) -# usertype SessionKey; secret k: Function; diff --git a/spdl/SPORE/kaochow-v3.spdl b/spdl/SPORE/kaochow-v3.spdl index 54bf862..7569ded 100644 --- a/spdl/SPORE/kaochow-v3.spdl +++ b/spdl/SPORE/kaochow-v3.spdl @@ -3,10 +3,6 @@ # Modelled after the description in the SPORE library # http://www.lsv.ens-cachan.fr/spore/kaoChow3.html # -# Note: -# This protocol uses a ticket so scyther will only be able to verify -# the protocol using the ARACHNE engine (-a) -# usertype SessionKey; usertype ExpiredTimeStamp; diff --git a/spdl/SPORE/kaochow.spdl b/spdl/SPORE/kaochow.spdl index 021397a..0657aed 100644 --- a/spdl/SPORE/kaochow.spdl +++ b/spdl/SPORE/kaochow.spdl @@ -3,10 +3,6 @@ # Modelled after the description in the SPORE library # http://www.lsv.ens-cachan.fr/spore/kaoChow1.html # -# Note: -# This protocol uses a ticket so scyther will only be able to verify -# the protocol using the ARACHNE engine (-a) -# usertype SessionKey; secret k: Function; diff --git a/spdl/SPORE/ksl-lowe.spdl b/spdl/SPORE/ksl-lowe.spdl index 3a5063b..662e9e9 100644 --- a/spdl/SPORE/ksl-lowe.spdl +++ b/spdl/SPORE/ksl-lowe.spdl @@ -4,10 +4,6 @@ # http://www.lsv.ens-cachan.fr/spore/kslLowe.html # # Note: -# This protocol uses a ticket so scyther will only be able to verify -# the protocol using the ARACHNE engine (-a) -# -# Note: # According to SPORE there are no attacks on this protocol, scyther # finds one however. This has to be investigated further. diff --git a/spdl/SPORE/ksl.spdl b/spdl/SPORE/ksl.spdl index dddf135..62b247e 100644 --- a/spdl/SPORE/ksl.spdl +++ b/spdl/SPORE/ksl.spdl @@ -3,9 +3,6 @@ # Modelled after the description in the SPORE library # http://www.lsv.ens-cachan.fr/spore/ksl.html # -# Note: -# This protocol uses a ticket so scyther will only be able to verify -# the protocol using the ARACHNE engine (-a) # diff --git a/spdl/SPORE/needham-schroeder-sk-amend.spdl b/spdl/SPORE/needham-schroeder-sk-amend.spdl index 7be987a..d593fd7 100644 --- a/spdl/SPORE/needham-schroeder-sk-amend.spdl +++ b/spdl/SPORE/needham-schroeder-sk-amend.spdl @@ -5,10 +5,6 @@ # # # Note: -# This protocol uses a ticket so scyther will only be able to verify -# the protocol using the ARACHNE engine (-a) -# -# Note: # According to SPORE there are no attacks on this protocol, scyther # finds one however. This has to be investigated further. diff --git a/spdl/SPORE/needham-schroeder-sk.spdl b/spdl/SPORE/needham-schroeder-sk.spdl index 5fb9a85..7ccee65 100644 --- a/spdl/SPORE/needham-schroeder-sk.spdl +++ b/spdl/SPORE/needham-schroeder-sk.spdl @@ -4,10 +4,6 @@ # http://www.lsv.ens-cachan.fr/spore/nssk.html # # -# Note: -# This protocol uses a ticket so scyther will only be able to verify -# the protocol using the ARACHNE engine (-a) -# secret k: Function; diff --git a/spdl/SPORE/neumannstub-guttman-hwang.spdl b/spdl/SPORE/neumannstub-guttman-hwang.spdl index f289224..8353535 100644 --- a/spdl/SPORE/neumannstub-guttman-hwang.spdl +++ b/spdl/SPORE/neumannstub-guttman-hwang.spdl @@ -4,10 +4,6 @@ # http://www.lsv.ens-cachan.fr/spore/neumannStubblebine.html # # Note: -# This protocol uses a ticket so scyther will only be able to verify -# the protocol using the ARACHNE engine (-a) -# -# Note: # In SPORE this protocol is not described correctly, there are in fact 2 # different protocols (the key establishment protocol and the repeated # authentication protocol) diff --git a/spdl/SPORE/neumannstub-guttman.spdl b/spdl/SPORE/neumannstub-guttman.spdl index 7d343b0..ce0443d 100644 --- a/spdl/SPORE/neumannstub-guttman.spdl +++ b/spdl/SPORE/neumannstub-guttman.spdl @@ -4,10 +4,6 @@ # http://www.lsv.ens-cachan.fr/spore/neumannStubblebine.html # # Note: -# This protocol uses a ticket so scyther will only be able to verify -# the protocol using the ARACHNE engine (-a) -# -# Note: # In SPORE this protocol is not described correctly, there are in fact 2 # different protocols (the key establishment protocol and the repeated # authentication protocol) diff --git a/spdl/SPORE/neumannstub-hwang.spdl b/spdl/SPORE/neumannstub-hwang.spdl index c079cf5..2a79550 100644 --- a/spdl/SPORE/neumannstub-hwang.spdl +++ b/spdl/SPORE/neumannstub-hwang.spdl @@ -4,10 +4,6 @@ # http://www.lsv.ens-cachan.fr/spore/neumannStubblebineHwang.html # # Note: -# This protocol uses a ticket so scyther will only be able to verify -# the protocol using the ARACHNE engine (-a) -# -# Note: # According to SPORE there are no attacks on this protocol, scyther # finds one however. This has to be investigated further. diff --git a/spdl/SPORE/neumannstub-keycompromise.spdl b/spdl/SPORE/neumannstub-keycompromise.spdl index e11d13d..5dd1aeb 100644 --- a/spdl/SPORE/neumannstub-keycompromise.spdl +++ b/spdl/SPORE/neumannstub-keycompromise.spdl @@ -4,10 +4,6 @@ # http://www.lsv.ens-cachan.fr/spore/neumannStubblebine.html # # Note: -# This protocol uses a ticket so scyther will only be able to verify -# the protocol using the ARACHNE engine (-a) -# -# Note: # In SPORE this protocol is not described correctly, there are in fact 2 # different protocols (the key establishment protocol and the repeated # authentication protocol) diff --git a/spdl/SPORE/neumannstub.spdl b/spdl/SPORE/neumannstub.spdl index 7c5e429..14bef8a 100644 --- a/spdl/SPORE/neumannstub.spdl +++ b/spdl/SPORE/neumannstub.spdl @@ -4,10 +4,6 @@ # http://www.lsv.ens-cachan.fr/spore/neumannStubblebine.html # # Note: -# This protocol uses a ticket so scyther will only be able to verify -# the protocol using the ARACHNE engine (-a) -# -# Note: # In SPORE this protocol is not described correctly, there are in fact 2 # different protocols (the key establishment protocol and the repeated # authentication protocol) diff --git a/spdl/SPORE/otwayrees.spdl b/spdl/SPORE/otwayrees.spdl index a2bee13..3d1c4b1 100644 --- a/spdl/SPORE/otwayrees.spdl +++ b/spdl/SPORE/otwayrees.spdl @@ -3,11 +3,6 @@ # Modelled after the description in the SPORE library # http://www.lsv.ens-cachan.fr/spore/otwayRees.html # -# -# Note: -# This protocol uses a ticket so scyther will only be able to verify -# the protocol using the ARACHNE engine (-a) -# secret const k : Function; diff --git a/spdl/SPORE/smartright.spdl b/spdl/SPORE/smartright.spdl index 3133457..e91c568 100644 --- a/spdl/SPORE/smartright.spdl +++ b/spdl/SPORE/smartright.spdl @@ -7,10 +7,6 @@ # According to SPORE there are no known attacks on this protocol # # Note: -# This protocol uses a ticket so scyther will only be able to verify -# the protocol using the ARACHNE engine (-a) -# -# Note: # Scyther finds an attack because the value of VoR in te last message can # be replaced with an arbitrary value diff --git a/spdl/SPORE/woo-lam-pi-1.spdl b/spdl/SPORE/woo-lam-pi-1.spdl index 811ef4a..6e08913 100644 --- a/spdl/SPORE/woo-lam-pi-1.spdl +++ b/spdl/SPORE/woo-lam-pi-1.spdl @@ -3,10 +3,6 @@ # Modelled after the description in the SPORE library # http://www.lsv.ens-cachan.fr/spore/wooLamPi1.html # -# Note: -# This protocol uses a ticket so scyther will only be able to verify -# the protocol using the ARACHNE engine (-a) -# secret k: Function; diff --git a/spdl/SPORE/woo-lam-pi-2.spdl b/spdl/SPORE/woo-lam-pi-2.spdl index 416946c..3a39ac0 100644 --- a/spdl/SPORE/woo-lam-pi-2.spdl +++ b/spdl/SPORE/woo-lam-pi-2.spdl @@ -3,10 +3,6 @@ # Modelled after the description in the SPORE library # http://www.lsv.ens-cachan.fr/spore/wooLamPi2.html # -# Note: -# This protocol uses a ticket so scyther will only be able to verify -# the protocol using the ARACHNE engine (-a) -# secret k: Function; diff --git a/spdl/SPORE/woo-lam-pi-3.spdl b/spdl/SPORE/woo-lam-pi-3.spdl index c930e81..b59027e 100644 --- a/spdl/SPORE/woo-lam-pi-3.spdl +++ b/spdl/SPORE/woo-lam-pi-3.spdl @@ -3,10 +3,6 @@ # Modelled after the description in the SPORE library # http://www.lsv.ens-cachan.fr/spore/wooLamPi3.html # -# Note: -# This protocol uses a ticket so scyther will only be able to verify -# the protocol using the ARACHNE engine (-a) -# secret k: Function; diff --git a/spdl/SPORE/woo-lam-pi-f.spdl b/spdl/SPORE/woo-lam-pi-f.spdl index a3ecd57..b0a0287 100644 --- a/spdl/SPORE/woo-lam-pi-f.spdl +++ b/spdl/SPORE/woo-lam-pi-f.spdl @@ -3,10 +3,6 @@ # Modelled after the description in the SPORE library # http://www.lsv.ens-cachan.fr/spore/wooLamPif.html # -# Note: -# This protocol uses a ticket so scyther will only be able to verify -# the protocol using the ARACHNE engine (-a) -# secret k: Function; diff --git a/spdl/SPORE/woo-lam-pi.spdl b/spdl/SPORE/woo-lam-pi.spdl index 04295f4..05c76ce 100644 --- a/spdl/SPORE/woo-lam-pi.spdl +++ b/spdl/SPORE/woo-lam-pi.spdl @@ -4,10 +4,6 @@ # http://www.lsv.ens-cachan.fr/spore/wooLamPi.html # # Note: -# This protocol uses a ticket so scyther will only be able to verify -# the protocol using the ARACHNE engine (-a) -# -# Note: # Scyther finds an attack that appears to be legit, but is not present in # SPORE. # diff --git a/spdl/SPORE/woo-lam.spdl b/spdl/SPORE/woo-lam.spdl index 8613167..a60ad71 100644 --- a/spdl/SPORE/woo-lam.spdl +++ b/spdl/SPORE/woo-lam.spdl @@ -3,10 +3,6 @@ # Modelled after the description in the SPORE library # http://www.lsv.ens-cachan.fr/spore/wooLamMutual.html # -# Note: -# This protocol uses a ticket so scyther will only be able to verify -# the protocol using the ARACHNE engine (-a) -# usertype SessionKey; diff --git a/spdl/SPORE/yahalom-ban.spdl b/spdl/SPORE/yahalom-ban.spdl index ef6d65a..c6908af 100644 --- a/spdl/SPORE/yahalom-ban.spdl +++ b/spdl/SPORE/yahalom-ban.spdl @@ -3,10 +3,6 @@ # Modelled after the description in the SPORE library # http://www.lsv.ens-cachan.fr/spore/yahalomBAN.html # -# Note: -# This protocol uses a ticket so scyther will only be able to verify -# the protocol using the ARACHNE engine (-a) -# secret k : Function; diff --git a/spdl/SPORE/yahalom-paulson.spdl b/spdl/SPORE/yahalom-paulson.spdl index e902ed9..86cb67e 100644 --- a/spdl/SPORE/yahalom-paulson.spdl +++ b/spdl/SPORE/yahalom-paulson.spdl @@ -3,9 +3,6 @@ # Modelled after the description in the SPORE library # http://www.lsv.ens-cachan.fr/spore/yahalomPaulson.html # -# Note: -# This protocol uses a ticket so scyther will only be able to verify -# the protocol using the ARACHNE engine (-a) # secret k : Function; diff --git a/spdl/SPORE/yahalom.spdl b/spdl/SPORE/yahalom.spdl index 57240d4..f8c05bf 100644 --- a/spdl/SPORE/yahalom.spdl +++ b/spdl/SPORE/yahalom.spdl @@ -3,9 +3,6 @@ # Modelled after the description in the SPORE library # http://www.lsv.ens-cachan.fr/spore/yahalom.html # -# Note: -# This protocol uses a ticket so scyther will only be able to verify -# the protocol using the ARACHNE engine (-a) # secret k : Function;