- Improvements troughout.

scripts/if2spdl/If.py

@@ -8,6 +8,12 @@ class Message(object):
 	def __cmp__(self,other):
 		return cmp(str(self),str(other))
 
+	def inTerms(self):
+		return self
+
+	def isVariable(self):
+		return False
+
 class Constant(Message):
 	def __init__ (self,type,s,optprime=""):
 		self.type = type
@@ -21,7 +27,8 @@ class Constant(Message):
 		return str(self)
 
 class Variable(Constant):
-	pass
+	def isVariable(self):
+		return True
 
 class PublicKey(Constant):
 	pass
@@ -34,6 +41,9 @@ class Composed(Message):
 	def __str__(self):
 		return "(" + str(self.left) + "," + str(self.right) + ")"
 
+	def inTerms(self):
+		return self.left.inTerms() + self.right.inTerms()
+
 class PublicCrypt(Message):
 	def __init__ (self,key,message):
 		self.key = key
@@ -42,19 +52,23 @@ class PublicCrypt(Message):
 	def __str__(self):
 		return "{" + str(self.message) + "}" + str(self.key) + " "
 
+	def inTerms(self):
+		return self.key.inTerms() + self.message.inTerms()
+
+
 class SymmetricCrypt(PublicCrypt):
 	pass
 
-class XOR(Message):
+class XOR(Composed):
-	def __init__ (self, m1,m2):
-		self.left = m1
-		self.right = m2
-	
 	def __str__(self):
 		return str(self.left) + " xor " + str(self.right)
 
+
 class MsgList(list):
-	pass
+	def inTerms(self):
+		l = []
+		for m in self:
+			l = l + m.inTerms()
 
 class Fact(list):
 	def __repr__(self):
@@ -121,12 +135,11 @@ class MessageFact(Fact):
 		return str(self)
 
 	def spdl(self):
-		res = "send_"		# TODO this might be a read!
+		res = ""
-		res += str(self.step)
 		res += "(" + str(self.claimsender)
 		res += "," + str(self.recipient)
 		res += ", " + str(self.message)
-		res += " );\n"
+		res += " )"
 		return res
 
 class State(list):
@@ -237,4 +250,23 @@ class AuthenticateRule(GoalRule):
 	def __str__(self):
 		return "Authenticate " + GoalRule.__str__(self)
 
+class Protocol(list):
+	def setFilename(self, filename):
+		# TODO untested
+		parts = filename.split("/")
+		self.path = "".join(parts[:-1])
+		self.filename = parts[-1]
+
+	# Get head of filename (until first dot)
+	def getBasename(self):
+		parts = self.filename.split(".")
+		if parts[0] == "":
+			return "None"
+		else:
+			return parts[0]
+
+	# Construct protocol name from filename
+	def getName(self):
+		return self.getBaseName()
+		
 

scripts/if2spdl/Ifparser.py

@@ -262,7 +262,6 @@ def ifParser():
 	# A complete file
 	parser = OneOrMore(labeledrule)
 	parser.ignore("##" + restOfLine)
-
 	return parser
 
 # Determine (un)typedness from this line
@@ -289,21 +288,28 @@ def typeSwitch(line):
 	str += "typed version."
 	print str
 
-# Parse an entire file, including the first one
+# Parse a number of lines, including the first line with the type switch
 def linesParse(lines):
 
 	typeSwitch(lines[0])
 	parser = ifParser()
-	return parser.parseString("".join( lines[1:]))
+	return If.Protocol(parser.parseString("".join( lines[1:])))
+
+# Parse an entire file
+#
+# Return a protocol
+def fileParse(filename):
+	file = open(filename, "r")
+	protocol = linesParse(file.readlines())
+	file.close()
+	protocol.setFilename(filename)
+	return protocol
 
 # Main code
 def main():
 	print "Testing Ifparser module"
 	print
-	file = open("NSPK_LOWE.if", "r")
+	print fileParse("NSPK_LOWE.if")
-	rulelist = linesParse(file.readlines())
-	file.close()
-	print rulelist
 
 if __name__ == '__main__':
 	main()

scripts/if2spdl/Spdl.py

@@ -5,31 +5,53 @@
 import If
 from misc import *
 
-def processRole(rulelist, role):
+def action(protocol, actiontype, rule, fact):
+	res = actiontype + "_"
+	res += str(fact.step)
+	res += fact.spdl()
+	res += ";\n"
+	return res
 
+def processRole(protocol, role):
+
+	res = ""
 	print "Role", role
-	for rule in rulelist:
+	# initial knowledge
+	for rule in protocol:
 		if role in rule.getActors():
-			for fact in rule.getFacts():
+			for fact in rule.left:
-				if type(fact) == If.MessageFact:
+				if type(fact) == If.PrincipalFact:
-					print fact.spdl()
+					print fact
 
-	print
+
+	# derive message sequence
+	for rule in protocol:
+		if role in rule.getActors():
+			for fact in rule.left:
+				if type(fact) == If.MessageFact:
+					res += action(protocol, "read", rule, fact)
+
+			for fact in rule.right:
+				if type(fact) == If.MessageFact:
+					res += action(protocol, "send", rule, fact)
+
+
+	print res
 	return ""
 
 
-def getRoles(rulelist):
+def getRoles(protocol):
 	roles = []
-	for rule in rulelist:
+	for rule in protocol:
 		roles += rule.getActors()
 	return uniq(roles)
 
-def generator(rulelist):
+def generator(protocol):
-	roles = getRoles(rulelist)
+	roles = getRoles(protocol)
-	print "Found",len(rulelist),"rules."
+	print "Found",len(protocol),"rules."
 	print "Roles:", roles
 	res = ""
 	for role in roles:
-		res += processRole(rulelist,role)
+		res += processRole(protocol,role)
 	return res
 

scripts/if2spdl/if2spdl.py

@@ -5,10 +5,8 @@ import Ifparser
 import Spdl
 
 def main():
-	file = open("NSPK_LOWE.if", "r")
+	protocol = Ifparser.fileParse("NSPK_LOWE.if")
-	rulelist = Ifparser.linesParse(file.readlines())
+	print Spdl.generator(protocol)
-	file.close()
-	print Spdl.generator(rulelist)
 
 if __name__ == "__main__":
 	main()