From f3f381cb36183c19ad306ea37726df69179f3299 Mon Sep 17 00:00:00 2001 From: ccremers Date: Mon, 5 Dec 2005 14:28:09 +0000 Subject: [PATCH] - Big progess. Nonces are renamed automatically, knowledge updates are handled. --- scripts/if2spdl/If.py | 68 +++++++++++++- scripts/if2spdl/Spdl.py | 198 ++++++++++++++++++++++++++++++++++++---- 2 files changed, 247 insertions(+), 19 deletions(-) diff --git a/scripts/if2spdl/If.py b/scripts/if2spdl/If.py index b852427..975a5d4 100644 --- a/scripts/if2spdl/If.py +++ b/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" diff --git a/scripts/if2spdl/Spdl.py b/scripts/if2spdl/Spdl.py index b436629..409c080 100644 --- a/scripts/if2spdl/Spdl.py +++ b/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 + " (" - # TODO Insert parameter agents - res += ")\n" - res += "{\n" + res += "\trole " + self.name + "\n" + res += "\t{\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 - res += "\t// Knowledge before: " + str(self.rules[0].before.knowledge) + "\n" + # Message sequence (based on rules) + 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