Updating the protocol generator for the ffgg family.

- Removed obsolete declarations, updating syntax conventions.
- Added a more useful origin comment.
This commit is contained in:
Cas Cremers 2013-11-18 16:59:11 +00:00
parent 1b04bf9274
commit 1a9b494f85

View File

@ -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