diff --git a/testing/ffgg_n/ffgg_n.py b/testing/ffgg_n/ffgg_n.py index 6ddbb9b..d620de3 100755 --- a/testing/ffgg_n/ffgg_n.py +++ b/testing/ffgg_n/ffgg_n.py @@ -1,7 +1,7 @@ #!/usr/bin/python """ Scyther : An automatic verifier for security protocols. - Copyright (C) 2007 Cas Cremers + Copyright (C) 2007-2013 Cas Cremers This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License @@ -18,6 +18,13 @@ Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301, USA. """ +""" + This program generates arbitrary members of the ffgg protocol family, as proposed + by Jonathan Millen in the paper "A Necessarily Parallel Attack". + By providing a number n as the input, the program outputs on stdout the + corresponding protocol ffgg_n. +""" + import sys def nlist(pref,post,si,ei): @@ -36,12 +43,6 @@ def ffgg(n): * ffgg%i protocol */ -// PKI infrastructure - -const pk: Function; -secret sk: Function; -inversekeys (pk,sk); - // The protocol description protocol ffgg%i(A,B) @@ -58,7 +59,7 @@ protocol ffgg%i(A,B) rconst = nonces1 s += """ - const M: Nonce; + fresh M: Nonce; var %s: Nonce; send_1(A,B, A ); @@ -72,7 +73,7 @@ protocol ffgg%i(A,B) role B { var M,%s: Nonce; - const %s: Nonce; + fresh %s: Nonce; read_1(A,B, A ); send_2(B,A, B,%s ); @@ -81,17 +82,6 @@ protocol ffgg%i(A,B) } } -// The agents in the system - -const Alice,Bob: Agent; - -// An untrusted agent, with leaked information - -const Eve: Agent; -untrusted Eve; -const ne: Nonce; -compromised sk(Eve); - """ % (ivar,nonces1,nonces1,nonces1b,rvar,rconst,nonces1,nonces2,nonces2) return s