- Big progess. Nonces are renamed automatically, knowledge updates are

handled.

scripts/if2spdl/If.py

@@ -4,16 +4,25 @@
 #
 #	Objects and stuff for the intermediate format
 #
+import copy	# To copy objects
+
+
 class Message(object):
 	def __cmp__(self,other):
 		return cmp(str(self),str(other))
 
 	def inTerms(self):
-		return self
+		return [self]
 
 	def isVariable(self):
 		return False
 
+	def substitute(self, msgfrom, msgto):
+		if self == msgfrom:
+			return msgto
+		else:
+			return self
+
 class Constant(Message):
 	def __init__ (self,type,s,optprime=""):
 		self.type = type
@@ -23,6 +32,9 @@ class Constant(Message):
 	def __str__(self):
 		return self.str + self.prime
 
+	def spdl(self,braces=True):
+		return self.str + self.prime
+
 	def __repr__(self):
 		return str(self)
 
@@ -41,9 +53,27 @@ class Composed(Message):
 	def __str__(self):
 		return "(" + str(self.left) + "," + str(self.right) + ")"
 
+	def spdl(self,braces=True):
+		res = ""
+		if braces:
+			res += "("
+		res += self.left.spdl(False) + "," + self.right.spdl(False)
+		if braces:
+			res += ")"
+		return res
+
 	def inTerms(self):
 		return self.left.inTerms() + self.right.inTerms()
 
+	def substitute(self, msgfrom, msgto):
+		if self == msgfrom:
+			return msgto
+		else:
+			new = copy.copy(self)
+			new.left = self.left.substitute(msgfrom, msgto)
+			new.right = self.right.substitute(msgfrom, msgto)
+			return new
+
 class PublicCrypt(Message):
 	def __init__ (self,key,message):
 		self.key = key
@@ -51,10 +81,22 @@ class PublicCrypt(Message):
 
 	def __str__(self):
 		return "{" + str(self.message) + "}" + str(self.key) + " "
+	
+	def spdl(self,braces=True):
+		return "{" + self.message.spdl(False) + "}" + self.key.spdl() + " "
 
 	def inTerms(self):
 		return self.key.inTerms() + self.message.inTerms()
 
+	def substitute(self, msgfrom, msgto):
+		if self == msgfrom:
+			return msgto
+		else:
+			new = copy.copy(self)
+			new.key = self.key.substitute(msgfrom, msgto)
+			new.message = self.message.substitute(msgfrom, msgto)
+			return new
+
 
 class SymmetricCrypt(PublicCrypt):
 	pass
@@ -63,22 +105,44 @@ class XOR(Composed):
 	def __str__(self):
 		return str(self.left) + " xor " + str(self.right)
 
+	def spdl(self,braces=True):
+		# This is not possible yet!
+		raise Error
+
 
 class MsgList(list):
 	def inTerms(self):
 		l = []
 		for m in self:
 			l = l + m.inTerms()
+		return l
 
 	def __str__(self):
 		return "[ " + ", ".join(map(str,self)) + " ]"
 
+	def spdl(self):
+		first = True
+		res = ""
+		for m in self:
+			if not first:
+				res += ", "
+			else:
+				first = False
+			res += m.spdl()
+		return res
+
 	def getList(self):
 		l = []
 		for e in self:
 			l.append(e)
 		return l
 
+	def substitute(self, msgfrom, msgto):
+		newl = []
+		for m in self:
+			newl.append(m.substitute(msgfrom, msgto))
+		return MsgList(newl)
+
 class Fact(list):
 	def __repr__(self):
 		return "Fact<" + list.__repr__(self) + ">"
@@ -300,7 +364,7 @@ class Protocol(list):
 		self.filename = parts[-1]
 
 	# Get head of filename (until first dot)
-	def getBasename(self):
+	def getBaseName(self):
 		parts = self.filename.split(".")
 		if parts[0] == "":
 			return "None"

scripts/if2spdl/Spdl.py

@@ -18,16 +18,59 @@ def getRoles(protocol):
 		roles += rule.getActors()
 	return uniq(roles)
 
+class Event(object):
+	""" SPDL role event """
+	def substitute(self, msgfrom, msgto):
+		pass
+
+	def spdl(self):
+		return str(self)
+
+class CommEvent(Event):
+	""" SPDL message event """
+	def __init__(self,type,label,fromrole,torole,message):
+		self.type = type
+		self.label = label
+		self.fromrole = fromrole
+		self.torole = torole
+		self.message = message
+
+	def substitute(self, msgfrom, msgto):
+		self.message = self.message.substitute(msgfrom, msgto)
+	
+	def spdl(self):
+		res = str(self.type) + "_"
+		res += str(self.label)
+		res += "("
+		res += self.fromrole.spdl()
+		res += ","
+		res += self.torole.spdl()
+		res += ", "
+		res += self.message.spdl(False)
+		res += " )"
+		return res
+
+	def inTerms(self):
+		l = []
+		l += self.fromrole.inTerms()
+		l += self.torole.inTerms()
+		l += self.message.inTerms()
+		return l
+
 class Role(object):
 	""" Containts a list of rules, to be executed sequentially """
 	def __init__(self,name,actor):
 		self.name = name
 		self.rules = []
 		self.actor = actor
+		self.events = []
+		self.knowledge = If.MsgList([])
+		self.constants = If.MsgList([])
+		self.variables = If.MsgList([])
 	
 	def prependRule(self,rule):
 		self.rules = [rule] + self.rules
-
+	
 	def getLength(self):
 		return len(self.rules)
 
@@ -50,38 +93,152 @@ class Role(object):
 			res += "\n\n"
 		return res
 
+	def appendEvent(self, event):
+		self.event += [event]
+
+	def inTerms(self):
+		l = []
+		for ev in self.events:
+			l += ev.inTerms()
+		return l
+
 	def spdl(self):
+		pf = "\t\t"
+		pfc = pf + "// "
+
+		# Start output
 		res = ""
 		if len(self.rules) == 0:
 			return res
-		res += "role " + self.name + " ("
+		res += "\trole " + self.name + "\n"
-		# TODO Insert parameter agents
+		res += "\t{\n"
-		res += ")\n"
+
-		res += "{\n"
+		
+
+
 		# TODO declare constants, variables
+		res += pfc + "Constants and variables\n"
+		res += pf + "const " + self.constants.spdl() + ";\n"
+		res += pf + "var   " + self.variables.spdl() + ";\n"
 		res += "\n"
-		# Message sequence
+		# Message sequence (based on rules)
-		res += "\t// Knowledge before: " + str(self.rules[0].before.knowledge) + "\n"
+		res += pfc + "Rule list based messages\n"
+		res += pfc + "Knowledge before: " + str(self.rules[0].before.knowledge) + "\n"
 		for rule in self.rules:
 			# Read
 			if rule.readFact != None:
-				res += "\t" + action("read",rule.readFact) + ";\n"
+				res += pfc + action("read",rule.readFact) + ";\n"
 			# Show knowledge extending for this read
-			res += "\t// Knowledge delta: " + str(rule.before.runknowledge) + " -> " + str(rule.after.runknowledge) + "\n"
+			res += pfc + "Knowledge delta: " + str(rule.before.runknowledge) + " -> " + str(rule.after.runknowledge) + "\n"
-
-
 
 			# Send
 			if rule.sendFact != None:
-				res += "\t" + action("send",rule.sendFact) + ";\n"
+				res += pfc + action("send",rule.sendFact) + ";\n"
+		res += "\n"
+
+		# Message sequence (based on event list)
+		res += pfc + "Event list based messages\n"
+		for event in self.events:
+			res += pf + event.spdl() + ";\n"
+		res += "\n"
+
 		# TODO claims
+		
 		# Close up
-		res += "}\n\n"
+		res += "\t}\n\n"
 		return res
 
 	def __cmp__(self,other):
 		return cmp(self.name, other.name)
 
+def sanitizeRole(protocol, role):
+	""" Get rid of If artefacts, and construct role.events """
+	rules = role.rules
+
+	# Create events for each rule
+	ruleevents = []
+	role.events = []
+	for rule in role.rules:
+		events = []
+		if rule.readFact != None:
+			f = rule.readFact
+			events.append(CommEvent("read", f.step, f.claimsender, f.recipient, f.message))
+		if rule.sendFact != None:
+			f = rule.sendFact
+			events.append(CommEvent("send", f.step, f.claimsender, f.recipient, f.message))
+		ruleevents.append(events)
+		role.events += events
+	
+	# Try to substitute stuff until sane
+	# First check whether knowledge lists actually agree in length,
+	# otherwise this does not make sense at all.
+	nmax = len(rules)-1
+	n = 0
+	while n < nmax:
+		knowbefore = rules[n].after.runknowledge
+		knowafter = rules[n+1].before.runknowledge
+		if len(knowbefore) != len(knowafter):
+			print "Error: Lengths differ for step", n
+		else:
+			# The after items should be substituted by the
+			# before items
+			i = 0
+			while i < len(knowbefore):
+				# Substitute this item
+				msgfrom = knowafter[i]
+				msgto = knowbefore[i]
+				if msgfrom != msgto:
+					### TEST
+					print "Substituting %s by %s" % (str(msgfrom), str(msgto))
+					# In all subsequent terms... TODO or
+					# just the next one?
+					j = n+1
+					while j < len(rules):
+						events = ruleevents[j]
+						for ev in events:
+							ev.substitute(msgfrom, msgto)
+						j = j+1
+				i = i + 1
+
+		n = n + 1
+
+	# Extract knowledge etc
+	role.knowledge = role.rules[0].before.knowledge
+	role.constants = If.MsgList([])
+	role.variables = If.MsgList([])
+	l = uniq(role.inTerms())
+	replacelist = []
+	noncecounter = 0
+	for t in l:
+		if t not in role.knowledge:
+			if t.isVariable():
+				role.variables.append(t)
+			else:
+				# For now, we say local constants from the intermediate
+				# format are simply replaced by
+				# local constants from the
+				# operational semantics. This is
+				# not necessarily correct. TODO
+				### constants.append(t)
+				cname = "n"
+				rname = role.name
+				if rname[0] == "x":
+					rname = rname[1:]
+				cname += rname
+				cname += str(noncecounter)
+				msg = If.Constant("nonce",cname)
+				noncecounter = noncecounter + 1
+				replacelist.append( (t,msg) )
+				role.constants.append(msg)
+	# Apply replacelist
+	if len(replacelist) > 0:
+		for ev in role.events:
+			for (f,t) in replacelist:
+				ev.substitute(f,t)
+
+
+		
+
 def extractRoles(protocol):
 	""" Extract the roles of a protocol description. This yields a
 	list of Role objects """
@@ -115,9 +272,6 @@ def extractRoles(protocol):
 		else:
 			actor = hrule.getActors()[0]
 			name = str(actor)
-			# Remove variable x prefix
-			if len(name) > 1 and name[0] == 'x':
-				name = name[1:]
 
 		# This name is maybe already taken
 		if name in rolenames:
@@ -154,14 +308,24 @@ def extractRoles(protocol):
 						# No loop, prepend
 						role.prependRule(rule)
 
+		# Role done, sanitize
+		sanitizeRole( protocol, role)
+
 	return roles
 
 def generator(protocol):
 	roles = extractRoles(protocol)
 	roles.sort()
 	res = ""
-	print "Found",len(roles),"roles."
+	res += "protocol " + protocol.getName() + " ("
+	namelist = []
+	for role in roles:
+		namelist += [role.name]
+	res += ", ".join(namelist)
+	res += ")\n"
+	res += "{\n"
 	for role in roles:
 		res += role.spdl()
+	res += "}\n"
 	return res