- Modified the multinsl generator to also be able to generate bke
variants (--protocol bke).
This commit is contained in:
ccremers
parent
aab5328a9b
commit
00e49601eb
@ -5,238 +5,282 @@
|
|||||||
# Input: P variant
|
# Input: P variant
|
||||||
#
|
#
|
||||||
# variant uses some bits:
|
# variant uses some bits:
|
||||||
# bit mask meaning if set to '1'
|
# bit mask meaning if set to '1'
|
||||||
# (message type 1)
|
# (message type 1)
|
||||||
# 0 1 nonces in reverse
|
# 0 1 nonces in reverse
|
||||||
# 1 2 nonces after agents
|
# 1 2 nonces after agents
|
||||||
# 2 4 agents in reverse
|
# 2 4 agents in reverse
|
||||||
# 3 8 interleaved variant
|
# 3 8 interleaved variant
|
||||||
# (message type 2)
|
# (message type 2)
|
||||||
# 4 16 nonces in reverse in message 2
|
# 4 16 nonces in reverse in message 2
|
||||||
#
|
#
|
||||||
# Convention similar to e.g. Prolog: capitals indicate open variables;
|
# Convention similar to e.g. Prolog: capitals indicate open variables;
|
||||||
# in particular, they can be bound by _any_ value during the run,
|
# in particular, they can be bound by _any_ value during the run,
|
||||||
# assuming full type flaws.
|
# assuming full type flaws.
|
||||||
#
|
#
|
||||||
import sys
|
import sys
|
||||||
|
from optparse import OptionParser
|
||||||
|
|
||||||
|
def parseArgs():
|
||||||
|
usage = "usage: %s [opts]" % sys.argv[0]
|
||||||
|
parser = OptionParser(usage=usage)
|
||||||
|
parser.add_option('-p','--protocol', dest='protocol',
|
||||||
|
help='Generate another protocol', default="nsl",
|
||||||
|
action='store')
|
||||||
|
(opts, args) = parser.parse_args()
|
||||||
|
if len(args) != 2:
|
||||||
|
parser.print_help()
|
||||||
|
sys.exit(0)
|
||||||
|
if opts.protocol not in ["nsl","bke"]:
|
||||||
|
print "I don't know the %s protocol." % (opts.protocol)
|
||||||
|
sys.exit(0)
|
||||||
|
return (opts,args)
|
||||||
|
|
||||||
|
|
||||||
def variablerole (r, inrole):
|
def variablerole (r, inrole):
|
||||||
if r == inrole or inrole == 0:
|
if r == inrole or inrole == 0:
|
||||||
return False
|
return False
|
||||||
else:
|
else:
|
||||||
return True
|
return True
|
||||||
|
|
||||||
def role (r,inrole):
|
def role (r,inrole):
|
||||||
global P
|
global P
|
||||||
|
|
||||||
return "r%i" % (r % P)
|
return "r%i" % (r % P)
|
||||||
|
|
||||||
|
def zeroconst ():
|
||||||
|
|
||||||
|
""" This is 0 or some other stupid constant """
|
||||||
|
|
||||||
|
return "zeroconst"
|
||||||
|
|
||||||
def nonce (r,inrole):
|
def nonce (r,inrole):
|
||||||
global P
|
global P
|
||||||
|
|
||||||
if r == inrole:
|
if r == inrole:
|
||||||
# nonce of our own
|
# nonce of our own
|
||||||
return "n%i" % (r % P)
|
return "n%i" % (r % P)
|
||||||
else:
|
else:
|
||||||
# a variable: we want to see this in the notation
|
# a variable: we want to see this in the notation
|
||||||
return "N%i" % (r % P)
|
return "N%i" % (r % P)
|
||||||
|
|
||||||
def extend (s1, s2):
|
def extend (s1, s2):
|
||||||
if s1 == "":
|
if s1 == "":
|
||||||
return s2
|
return s2
|
||||||
else:
|
else:
|
||||||
return s1 + "," + s2
|
return s1 + "," + s2
|
||||||
|
|
||||||
def weavel (l1,l2,reverse1,swap,reverse2,interleave):
|
def weavel (l1,l2,reverse1,swap,reverse2,interleave):
|
||||||
""" l1 is typically a list of nonces, l2 might be empty (names) """
|
""" l1 is typically a list of nonces, l2 might be empty (names) """
|
||||||
global variant
|
global variant
|
||||||
|
|
||||||
if reverse1:
|
if reverse1:
|
||||||
l1.reverse()
|
l1.reverse()
|
||||||
if l2 == []:
|
if l2 == []:
|
||||||
return l1
|
return l1
|
||||||
else:
|
else:
|
||||||
if reverse2:
|
if reverse2:
|
||||||
l2.reverse()
|
l2.reverse()
|
||||||
if swap:
|
if swap:
|
||||||
# swap
|
# swap
|
||||||
l3 = l1
|
l3 = l1
|
||||||
l1 = l2
|
l1 = l2
|
||||||
l2 = l3
|
l2 = l3
|
||||||
if interleave:
|
if interleave:
|
||||||
rl = []
|
rl = []
|
||||||
largest = max(len(l1),len(l2))
|
largest = max(len(l1),len(l2))
|
||||||
for i in range (0,largest):
|
for i in range (0,largest):
|
||||||
if i < len(l1):
|
if i < len(l1):
|
||||||
rl.append(l1[i])
|
rl.append(l1[i])
|
||||||
if i < len(l2):
|
if i < len(l2):
|
||||||
rl.append(l2[i])
|
rl.append(l2[i])
|
||||||
return rl
|
return rl
|
||||||
else:
|
else:
|
||||||
return l1 + l2
|
return l1 + l2
|
||||||
|
|
||||||
def message1 (label,inrole):
|
def message1 (label,inrole):
|
||||||
global P,variant
|
global P,variant
|
||||||
|
|
||||||
noncelist = []
|
noncelist = []
|
||||||
for i in range(0,label+1):
|
for i in range(0,label+1):
|
||||||
noncelist.append(nonce(i,inrole))
|
noncelist.append(nonce(i,inrole))
|
||||||
rolelist = []
|
rolelist = []
|
||||||
for i in range(0,P):
|
for i in range(0,P):
|
||||||
if i != (label+1) % P:
|
if i != (label+1) % P:
|
||||||
rolelist.append(role(i,inrole))
|
rolelist.append(role(i,inrole))
|
||||||
|
|
||||||
return ",".join(weavel(noncelist,rolelist,
|
return ",".join(weavel(noncelist,rolelist,
|
||||||
(variant & 1 != 0),
|
(variant & 1 != 0),
|
||||||
(variant & 2 != 0),
|
(variant & 2 != 0),
|
||||||
(variant & 4 != 0),
|
(variant & 4 != 0),
|
||||||
(variant & 8 != 0)
|
(variant & 8 != 0)
|
||||||
))
|
))
|
||||||
|
|
||||||
def message2 (label,inrole):
|
def message2 (label,inrole):
|
||||||
global P,variant
|
global P,variant,opts
|
||||||
|
|
||||||
noncelist = []
|
if opts.protocol == "nsl":
|
||||||
for i in range (((label + 1) % P),P):
|
noncelist = []
|
||||||
noncelist.append(nonce(i,inrole))
|
for i in range (((label + 1) % P),P):
|
||||||
|
noncelist.append(nonce(i,inrole))
|
||||||
|
|
||||||
return ",".join(weavel(noncelist,[],
|
return ",".join(weavel(noncelist,[],
|
||||||
(variant & 16 != 0),
|
(variant & 16 != 0),
|
||||||
False,
|
False,
|
||||||
False,
|
False,
|
||||||
False
|
False
|
||||||
))
|
))
|
||||||
|
elif opts.protocol == "bke":
|
||||||
|
noncelist = []
|
||||||
|
for i in range (((label + 1) % P) + 1,P):
|
||||||
|
noncelist.append(nonce(i,inrole))
|
||||||
|
if len(noncelist) == 0:
|
||||||
|
noncelist.append(zeroconst())
|
||||||
|
|
||||||
|
return ",".join(weavel(noncelist,[],
|
||||||
|
(variant & 16 != 0),
|
||||||
|
False,
|
||||||
|
False,
|
||||||
|
False
|
||||||
|
))
|
||||||
|
else:
|
||||||
|
print "Hmm, I don't know how to create the final message for protocol %s" % (opts.protocol)
|
||||||
|
|
||||||
def message (label,inrole):
|
def message (label,inrole):
|
||||||
global P
|
global P,opts
|
||||||
|
|
||||||
s = "{ "
|
s = "{ "
|
||||||
if label < P:
|
if label < P:
|
||||||
s = s + message1 (label,inrole)
|
s = s + message1 (label,inrole)
|
||||||
else:
|
else:
|
||||||
s = s + message2 (label,inrole)
|
s = s + message2 (label,inrole)
|
||||||
|
|
||||||
s = s + " }pk(%s)" % role(label+1,inrole)
|
if opts.protocol == "bke" and not (label < P):
|
||||||
return s
|
s = s + " }" + nonce((label+1) % P, inrole)
|
||||||
|
else:
|
||||||
|
s = s + " }pk(%s)" % role(label+1,inrole)
|
||||||
|
return s
|
||||||
|
|
||||||
def action (event,label,inrole):
|
def action (event,label,inrole):
|
||||||
s = "\t\t%s_%i(%s,%s, " % (event,label, role(label,inrole),
|
s = "\t\t%s_%i(%s,%s, " % (event,label, role(label,inrole),
|
||||||
role(label+1,inrole))
|
role(label+1,inrole))
|
||||||
s += message (label,inrole)
|
s += message (label,inrole)
|
||||||
s += " );\n"
|
s += " );\n"
|
||||||
return s
|
return s
|
||||||
|
|
||||||
def read (label,inrole):
|
def read (label,inrole):
|
||||||
return action ("read", label,inrole)
|
return action ("read", label,inrole)
|
||||||
|
|
||||||
|
|
||||||
def send (label,inrole):
|
def send (label,inrole):
|
||||||
return action ("send", label,inrole)
|
return action ("send", label,inrole)
|
||||||
|
|
||||||
def roledef (r):
|
def roledef (r):
|
||||||
global P
|
global P
|
||||||
|
|
||||||
s = ""
|
s = ""
|
||||||
s += "\trole " + role(r,r) + "\n\t{\n"
|
s += "\trole " + role(r,r) + "\n\t{\n"
|
||||||
|
|
||||||
# constants for this role
|
# constants for this role
|
||||||
|
|
||||||
s += "\t\tconst " + nonce (r,r) + ": Nonce;\n"
|
s += "\t\tconst " + nonce (r,r) + ": Nonce;\n"
|
||||||
|
|
||||||
# variables
|
# variables
|
||||||
|
|
||||||
s += "\t\tvar "
|
s += "\t\tvar "
|
||||||
nr = 0
|
nr = 0
|
||||||
for i in range (0,P):
|
for i in range (0,P):
|
||||||
if r != i:
|
if r != i:
|
||||||
if nr > 0:
|
if nr > 0:
|
||||||
s += ","
|
s += ","
|
||||||
s += nonce(i,r)
|
s += nonce(i,r)
|
||||||
nr += 1
|
nr += 1
|
||||||
|
|
||||||
s += ": Nonce;\n"
|
s += ": Nonce;\n"
|
||||||
|
|
||||||
# implicit role variables
|
# implicit role variables
|
||||||
|
|
||||||
rolevars = []
|
rolevars = []
|
||||||
for i in range (0,P):
|
for i in range (0,P):
|
||||||
if variablerole(i,r):
|
if variablerole(i,r):
|
||||||
rolevars.append(role(i,r))
|
rolevars.append(role(i,r))
|
||||||
|
|
||||||
if rolevars != []:
|
if rolevars != []:
|
||||||
s += "\t\t// Implicit role variables: "
|
s += "\t\t// Implicit role variables: "
|
||||||
s += ",".join(rolevars)
|
s += ",".join(rolevars)
|
||||||
s += ": Role;\n"
|
s += ": Role;\n"
|
||||||
|
|
||||||
# actions
|
# actions
|
||||||
|
|
||||||
s += "\n"
|
s += "\n"
|
||||||
if r > 0:
|
if r > 0:
|
||||||
# Initial read
|
# Initial read
|
||||||
s += read(r-1,r)
|
s += read(r-1,r)
|
||||||
s += send(r,r)
|
s += send(r,r)
|
||||||
s += read(P+r-1,r)
|
s += read(P+r-1,r)
|
||||||
if r < (P-1):
|
if r < (P-1):
|
||||||
# Final send
|
# Final send
|
||||||
s += send(P+r,r)
|
s += send(P+r,r)
|
||||||
|
|
||||||
# claims
|
# claims
|
||||||
|
|
||||||
s += "\t\tclaim_%sa( %s, Secret, %s );\n" % (role(r,r), role(r,r),
|
s += "\t\tclaim_%sa( %s, Secret, %s );\n" % (role(r,r), role(r,r),
|
||||||
nonce(r,r))
|
nonce(r,r))
|
||||||
s += "\t\tclaim_%sb( %s, Nisynch );\n" % (role(r,r), role(r,r))
|
s += "\t\tclaim_%sb( %s, Nisynch );\n" % (role(r,r), role(r,r))
|
||||||
|
|
||||||
# close
|
# close
|
||||||
s += "\t}\n\n"
|
s += "\t}\n\n"
|
||||||
return s
|
return s
|
||||||
|
|
||||||
|
|
||||||
def protocol (pset,vset):
|
def protocol (args):
|
||||||
global P,variant
|
global P,variant,opts
|
||||||
|
|
||||||
P = pset
|
P = int(args[0])
|
||||||
variant = vset
|
variant = int(args[1])
|
||||||
|
|
||||||
s = ""
|
s = ""
|
||||||
s += "// Generalized Needham-Schroeder-Lowe for %i parties\n\n" % P
|
s += "// Generalized %s protocol for %i parties\n\n" % (opts.protocol,P)
|
||||||
s += "// Variant %i\n" % variant
|
s += "// " + str(opts) + "\n\n"
|
||||||
s += "const pk: Function;\n"
|
s += "// Variant %i\n" % variant
|
||||||
s += "secret sk: Function;\n"
|
s += "const pk: Function;\n"
|
||||||
s += "inversekeys (pk,sk);\n\n"
|
s += "secret sk: Function;\n"
|
||||||
|
s += "inversekeys (pk,sk);\n"
|
||||||
|
|
||||||
|
if opts.protocol == "bke":
|
||||||
|
s += "usertype Globalconstant;\n"
|
||||||
|
s += "const %s: Globalconstant;\n" % (zeroconst())
|
||||||
|
|
||||||
s += "protocol mnsl%iv%i(" % (P,variant)
|
s += "\n"
|
||||||
for i in range (0,P):
|
|
||||||
if i > 0:
|
|
||||||
s += ","
|
|
||||||
s += role(i,i)
|
|
||||||
s += ")\n{\n"
|
|
||||||
|
|
||||||
for i in range (0,P):
|
s += "protocol mnsl%iv%i(" % (P,variant)
|
||||||
s += roledef(i)
|
for i in range (0,P):
|
||||||
|
if i > 0:
|
||||||
s += "}\n\n"
|
s += ","
|
||||||
|
s += role(i,i)
|
||||||
|
s += ")\n{\n"
|
||||||
|
|
||||||
s += "const Alice, Bob: Agent;\n\n"
|
for i in range (0,P):
|
||||||
|
s += roledef(i)
|
||||||
|
|
||||||
|
s += "}\n\n"
|
||||||
|
|
||||||
s += "const Eve: Agent;\n"
|
s += "const Alice, Bob: Agent;\n\n"
|
||||||
s += "untrusted Eve;\n"
|
|
||||||
s += "const ne: Nonce;\n"
|
|
||||||
s += "compromised sk(Eve);\n"
|
|
||||||
|
|
||||||
s += "\n"
|
s += "const Eve: Agent;\n"
|
||||||
return s
|
s += "untrusted Eve;\n"
|
||||||
|
s += "const ne: Nonce;\n"
|
||||||
|
s += "compromised sk(Eve);\n"
|
||||||
|
|
||||||
|
s += "\n"
|
||||||
|
return s
|
||||||
|
|
||||||
def main():
|
def main():
|
||||||
if len(sys.argv) < 3:
|
global opts
|
||||||
print "We need at least 2 arguments: number of parties, and variant"
|
|
||||||
print "Note that variant is in [0..31]"
|
(opts,args) = parseArgs()
|
||||||
print ""
|
print protocol(args)
|
||||||
print "E.g. './multinsl-generator.py 2 0' yields a default NSL protocol"
|
|
||||||
else:
|
|
||||||
print protocol(int (sys.argv[1]), int(sys.argv[2]))
|
|
||||||
|
|
||||||
# Only if main stuff
|
# Only if main stuff
|
||||||
if __name__ == '__main__':
|
if __name__ == '__main__':
|
||||||
main()
|
main()
|
||||||
else:
|
|
||||||
print protocol (2,0)
|
|
||||||
|
|||||||
@ -29,7 +29,7 @@ def tuplingchoice(variant,P,runs,latupling):
|
|||||||
s += " | scyther -a -r%i -m2 --summary %s" % (runs, extraflags)
|
s += " | scyther -a -r%i -m2 --summary %s" % (runs, extraflags)
|
||||||
#s += " | scyther -a -r%i --summary" % runs
|
#s += " | scyther -a -r%i --summary" % runs
|
||||||
#print s
|
#print s
|
||||||
s += " | grep \"failed:\""
|
s += " | grep \"complete_proof\""
|
||||||
out = commands.getoutput(s)
|
out = commands.getoutput(s)
|
||||||
if out == "":
|
if out == "":
|
||||||
#print "Okay"
|
#print "Okay"
|
||||||
|
|||||||
Loading…
Reference in New Issue
Block a user