- Removed obsolete reports of Arachne requirements.
This commit is contained in:
parent
6d7b2a2d73
commit
bd7dd7f92b
@ -4,10 +4,6 @@
|
|||||||
# http://www.lsv.ens-cachan.fr/spore/denningSaccoLowe.html
|
# http://www.lsv.ens-cachan.fr/spore/denningSaccoLowe.html
|
||||||
#
|
#
|
||||||
# Note:
|
# 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
|
# According to SPORE there are no attacks on this protocol, scyther
|
||||||
# finds one however. This has to be investigated further.
|
# finds one however. This has to be investigated further.
|
||||||
|
|
||||||
|
@ -3,10 +3,6 @@
|
|||||||
# Modelled after the description in the SPORE library
|
# Modelled after the description in the SPORE library
|
||||||
# http://www.lsv.ens-cachan.fr/spore/denningSacco.html
|
# 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 Key;
|
||||||
usertype SessionKey;
|
usertype SessionKey;
|
||||||
|
@ -3,10 +3,6 @@
|
|||||||
# Modelled after the description in the SPORE library
|
# Modelled after the description in the SPORE library
|
||||||
# http://www.lsv.ens-cachan.fr/spore/kaoChow2.html
|
# 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;
|
usertype SessionKey;
|
||||||
secret k: Function;
|
secret k: Function;
|
||||||
|
@ -3,10 +3,6 @@
|
|||||||
# Modelled after the description in the SPORE library
|
# Modelled after the description in the SPORE library
|
||||||
# http://www.lsv.ens-cachan.fr/spore/kaoChow3.html
|
# 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 SessionKey;
|
||||||
usertype ExpiredTimeStamp;
|
usertype ExpiredTimeStamp;
|
||||||
|
@ -3,10 +3,6 @@
|
|||||||
# Modelled after the description in the SPORE library
|
# Modelled after the description in the SPORE library
|
||||||
# http://www.lsv.ens-cachan.fr/spore/kaoChow1.html
|
# 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;
|
usertype SessionKey;
|
||||||
secret k: Function;
|
secret k: Function;
|
||||||
|
@ -4,10 +4,6 @@
|
|||||||
# http://www.lsv.ens-cachan.fr/spore/kslLowe.html
|
# http://www.lsv.ens-cachan.fr/spore/kslLowe.html
|
||||||
#
|
#
|
||||||
# Note:
|
# 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
|
# According to SPORE there are no attacks on this protocol, scyther
|
||||||
# finds one however. This has to be investigated further.
|
# finds one however. This has to be investigated further.
|
||||||
|
|
||||||
|
@ -3,9 +3,6 @@
|
|||||||
# Modelled after the description in the SPORE library
|
# Modelled after the description in the SPORE library
|
||||||
# http://www.lsv.ens-cachan.fr/spore/ksl.html
|
# 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)
|
|
||||||
#
|
#
|
||||||
|
|
||||||
|
|
||||||
|
@ -5,10 +5,6 @@
|
|||||||
#
|
#
|
||||||
#
|
#
|
||||||
# Note:
|
# 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
|
# According to SPORE there are no attacks on this protocol, scyther
|
||||||
# finds one however. This has to be investigated further.
|
# finds one however. This has to be investigated further.
|
||||||
|
|
||||||
|
@ -4,10 +4,6 @@
|
|||||||
# http://www.lsv.ens-cachan.fr/spore/nssk.html
|
# 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;
|
secret k: Function;
|
||||||
|
@ -4,10 +4,6 @@
|
|||||||
# http://www.lsv.ens-cachan.fr/spore/neumannStubblebine.html
|
# http://www.lsv.ens-cachan.fr/spore/neumannStubblebine.html
|
||||||
#
|
#
|
||||||
# Note:
|
# 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
|
# In SPORE this protocol is not described correctly, there are in fact 2
|
||||||
# different protocols (the key establishment protocol and the repeated
|
# different protocols (the key establishment protocol and the repeated
|
||||||
# authentication protocol)
|
# authentication protocol)
|
||||||
|
@ -4,10 +4,6 @@
|
|||||||
# http://www.lsv.ens-cachan.fr/spore/neumannStubblebine.html
|
# http://www.lsv.ens-cachan.fr/spore/neumannStubblebine.html
|
||||||
#
|
#
|
||||||
# Note:
|
# 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
|
# In SPORE this protocol is not described correctly, there are in fact 2
|
||||||
# different protocols (the key establishment protocol and the repeated
|
# different protocols (the key establishment protocol and the repeated
|
||||||
# authentication protocol)
|
# authentication protocol)
|
||||||
|
@ -4,10 +4,6 @@
|
|||||||
# http://www.lsv.ens-cachan.fr/spore/neumannStubblebineHwang.html
|
# http://www.lsv.ens-cachan.fr/spore/neumannStubblebineHwang.html
|
||||||
#
|
#
|
||||||
# Note:
|
# 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
|
# According to SPORE there are no attacks on this protocol, scyther
|
||||||
# finds one however. This has to be investigated further.
|
# finds one however. This has to be investigated further.
|
||||||
|
|
||||||
|
@ -4,10 +4,6 @@
|
|||||||
# http://www.lsv.ens-cachan.fr/spore/neumannStubblebine.html
|
# http://www.lsv.ens-cachan.fr/spore/neumannStubblebine.html
|
||||||
#
|
#
|
||||||
# Note:
|
# 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
|
# In SPORE this protocol is not described correctly, there are in fact 2
|
||||||
# different protocols (the key establishment protocol and the repeated
|
# different protocols (the key establishment protocol and the repeated
|
||||||
# authentication protocol)
|
# authentication protocol)
|
||||||
|
@ -4,10 +4,6 @@
|
|||||||
# http://www.lsv.ens-cachan.fr/spore/neumannStubblebine.html
|
# http://www.lsv.ens-cachan.fr/spore/neumannStubblebine.html
|
||||||
#
|
#
|
||||||
# Note:
|
# 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
|
# In SPORE this protocol is not described correctly, there are in fact 2
|
||||||
# different protocols (the key establishment protocol and the repeated
|
# different protocols (the key establishment protocol and the repeated
|
||||||
# authentication protocol)
|
# authentication protocol)
|
||||||
|
@ -3,11 +3,6 @@
|
|||||||
# Modelled after the description in the SPORE library
|
# Modelled after the description in the SPORE library
|
||||||
# http://www.lsv.ens-cachan.fr/spore/otwayRees.html
|
# 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;
|
secret const k : Function;
|
||||||
|
@ -7,10 +7,6 @@
|
|||||||
# According to SPORE there are no known attacks on this protocol
|
# According to SPORE there are no known attacks on this protocol
|
||||||
#
|
#
|
||||||
# Note:
|
# 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
|
# Scyther finds an attack because the value of VoR in te last message can
|
||||||
# be replaced with an arbitrary value
|
# be replaced with an arbitrary value
|
||||||
|
|
||||||
|
@ -3,10 +3,6 @@
|
|||||||
# Modelled after the description in the SPORE library
|
# Modelled after the description in the SPORE library
|
||||||
# http://www.lsv.ens-cachan.fr/spore/wooLamPi1.html
|
# 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;
|
secret k: Function;
|
||||||
|
|
||||||
|
@ -3,10 +3,6 @@
|
|||||||
# Modelled after the description in the SPORE library
|
# Modelled after the description in the SPORE library
|
||||||
# http://www.lsv.ens-cachan.fr/spore/wooLamPi2.html
|
# 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;
|
secret k: Function;
|
||||||
|
|
||||||
|
@ -3,10 +3,6 @@
|
|||||||
# Modelled after the description in the SPORE library
|
# Modelled after the description in the SPORE library
|
||||||
# http://www.lsv.ens-cachan.fr/spore/wooLamPi3.html
|
# 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;
|
secret k: Function;
|
||||||
|
|
||||||
|
@ -3,10 +3,6 @@
|
|||||||
# Modelled after the description in the SPORE library
|
# Modelled after the description in the SPORE library
|
||||||
# http://www.lsv.ens-cachan.fr/spore/wooLamPif.html
|
# 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;
|
secret k: Function;
|
||||||
|
|
||||||
|
@ -4,10 +4,6 @@
|
|||||||
# http://www.lsv.ens-cachan.fr/spore/wooLamPi.html
|
# http://www.lsv.ens-cachan.fr/spore/wooLamPi.html
|
||||||
#
|
#
|
||||||
# Note:
|
# 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
|
# Scyther finds an attack that appears to be legit, but is not present in
|
||||||
# SPORE.
|
# SPORE.
|
||||||
#
|
#
|
||||||
|
@ -3,10 +3,6 @@
|
|||||||
# Modelled after the description in the SPORE library
|
# Modelled after the description in the SPORE library
|
||||||
# http://www.lsv.ens-cachan.fr/spore/wooLamMutual.html
|
# 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;
|
usertype SessionKey;
|
||||||
|
@ -3,10 +3,6 @@
|
|||||||
# Modelled after the description in the SPORE library
|
# Modelled after the description in the SPORE library
|
||||||
# http://www.lsv.ens-cachan.fr/spore/yahalomBAN.html
|
# 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;
|
secret k : Function;
|
||||||
|
|
||||||
|
@ -3,9 +3,6 @@
|
|||||||
# Modelled after the description in the SPORE library
|
# Modelled after the description in the SPORE library
|
||||||
# http://www.lsv.ens-cachan.fr/spore/yahalomPaulson.html
|
# 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;
|
secret k : Function;
|
||||||
|
@ -3,9 +3,6 @@
|
|||||||
# Modelled after the description in the SPORE library
|
# Modelled after the description in the SPORE library
|
||||||
# http://www.lsv.ens-cachan.fr/spore/yahalom.html
|
# 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;
|
secret k : Function;
|
||||||
|
Loading…
Reference in New Issue
Block a user