diff --git a/scripts/if2spdl/If.py b/scripts/if2spdl/If.py index edffbaf..80be79e 100644 --- a/scripts/if2spdl/If.py +++ b/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): - def __init__ (self, m1,m2): - self.left = m1 - self.right = m2 - +class XOR(Composed): 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 += str(self.step) + res = "" 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() + diff --git a/scripts/if2spdl/Ifparser.py b/scripts/if2spdl/Ifparser.py index 3049a4a..5a25d2f 100755 --- a/scripts/if2spdl/Ifparser.py +++ b/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") - rulelist = linesParse(file.readlines()) - file.close() - print rulelist + print fileParse("NSPK_LOWE.if") if __name__ == '__main__': main() diff --git a/scripts/if2spdl/Spdl.py b/scripts/if2spdl/Spdl.py index 2ef3708..5ebd07e 100644 --- a/scripts/if2spdl/Spdl.py +++ b/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(): - if type(fact) == If.MessageFact: - print fact.spdl() + for fact in rule.left: + if type(fact) == If.PrincipalFact: + 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): - roles = getRoles(rulelist) - print "Found",len(rulelist),"rules." +def generator(protocol): + roles = getRoles(protocol) + print "Found",len(protocol),"rules." print "Roles:", roles res = "" for role in roles: - res += processRole(rulelist,role) + res += processRole(protocol,role) return res diff --git a/scripts/if2spdl/if2spdl.py b/scripts/if2spdl/if2spdl.py index 35ca54c..5caa6d7 100755 --- a/scripts/if2spdl/if2spdl.py +++ b/scripts/if2spdl/if2spdl.py @@ -5,10 +5,8 @@ import Ifparser import Spdl def main(): - file = open("NSPK_LOWE.if", "r") - rulelist = Ifparser.linesParse(file.readlines()) - file.close() - print Spdl.generator(rulelist) + protocol = Ifparser.fileParse("NSPK_LOWE.if") + print Spdl.generator(protocol) if __name__ == "__main__": main()