scyther/scripts/if2spdl/If.py

390 lines
7.9 KiB
Python
Raw Normal View History

2005-12-03 16:12:58 +00:00
#!/usr/bin/python
#
# If.py
#
# Objects and stuff for the intermediate format
#
import copy # To copy objects
2005-12-05 15:51:25 +00:00
import os # For path functions
class Message(object):
2005-12-04 14:46:37 +00:00
def __cmp__(self,other):
return cmp(str(self),str(other))
2005-12-04 18:42:24 +00:00
def inTerms(self):
return [self]
2005-12-04 18:42:24 +00:00
def isVariable(self):
return False
def substitute(self, msgfrom, msgto):
if self == msgfrom:
return msgto
else:
return self
def aKeys(self):
return []
class Constant(Message):
def __init__ (self,type,s,optprime=""):
2005-12-03 16:12:58 +00:00
self.type = type
self.prime = optprime
self.str = s
2005-12-03 16:12:58 +00:00
def __str__(self):
return self.str + self.prime
2005-12-03 16:12:58 +00:00
def spdl(self,braces=True):
return self.str + self.prime
2005-12-03 16:12:58 +00:00
def __repr__(self):
return str(self)
class Variable(Constant):
2005-12-04 18:42:24 +00:00
def isVariable(self):
return True
class PublicKey(Constant):
pass
2005-12-03 16:12:58 +00:00
class Composed(Message):
def __init__ (self,m1,m2):
self.left = m1
self.right = m2
def __str__(self):
return "(" + str(self.left) + "," + str(self.right) + ")"
2005-12-03 16:12:58 +00:00
def spdl(self,braces=True):
res = ""
if braces:
res += "("
res += self.left.spdl(False) + "," + self.right.spdl(False)
if braces:
res += ")"
return res
2005-12-04 18:42:24 +00:00
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
def aKeys(self):
return self.left.aKeys() + self.right.aKeys()
class SPCrypt(Message):
def __init__ (self,key,message):
self.key = key
self.message = message
2005-12-03 16:12:58 +00:00
def __str__(self):
return "{" + str(self.message) + "}" + str(self.key) + " "
def spdl(self,braces=True):
return "{" + self.message.spdl(False) + "}" + self.key.spdl() + " "
2005-12-04 18:42:24 +00:00
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
def aKeys(self):
return self.message.aKeys() + self.key.aKeys()
class PublicCrypt(SPCrypt):
def aKeys(self):
return self.message.aKeys() + [self.key]
2005-12-04 18:42:24 +00:00
class SymmetricCrypt(SPCrypt):
pass
2005-12-03 16:12:58 +00:00
2005-12-04 18:42:24 +00:00
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
2005-12-04 18:42:24 +00:00
2005-12-03 16:12:58 +00:00
class MsgList(list):
2005-12-04 18:42:24 +00:00
def inTerms(self):
l = []
for m in self:
l = l + m.inTerms()
return l
2005-12-03 16:12:58 +00:00
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)
2005-12-03 16:12:58 +00:00
class Fact(list):
def __repr__(self):
return "Fact<" + list.__repr__(self) + ">"
2005-12-04 14:46:37 +00:00
def getActor(self):
return None
2005-12-03 16:48:10 +00:00
class GoalFact(Fact):
def __repr__(self):
return "Goal " + Fact.__repr__(self)
class PrincipalFact(Fact):
2005-12-04 14:46:37 +00:00
def __init__(self,t):
self.step = t[0]
self.readnextfrom = t[1]
self.actor = t[2]
self.runknowledge = t[3]
self.knowledge = t[4]
self.bool = t[5]
self.session = t[6]
2005-12-03 16:48:10 +00:00
def __str__(self):
res = "Principal Fact:"
2005-12-04 14:46:37 +00:00
res += "\nStep " + str(self.step)
res += "\nReadNextFrom " + str(self.readnextfrom)
res += "\nActor " + str(self.actor)
res += "\nRunKnowledge " + str(self.runknowledge)
res += "\nKnowledge " + str(self.knowledge)
#res += "\nBool " + str(self.bool)
res += "\nSession " + str(self.session)
2005-12-03 16:48:10 +00:00
return res + "\n"
def __repr__(self):
return str(self)
2005-12-04 14:46:37 +00:00
def getActor(self):
return self.actor
2005-12-03 16:48:10 +00:00
class TimeFact(Fact):
def __repr__(self):
return "Time " + Fact.__repr__(self)
class MessageFact(Fact):
def __init__(self,t):
self.step = t[0]
self.realsender = t[1]
self.claimsender = t[2]
self.recipient = t[3]
self.message = t[4]
self.session = t[5]
2005-12-03 16:48:10 +00:00
def __str__(self):
res = "Message Fact:"
res += "\nStep " + str(self.step)
res += "\nRealSender " + str(self.realsender)
res += "\nClaimSender " + str(self.claimsender)
res += "\nRecipient " + str(self.recipient)
res += "\nMessage " + str(self.message)
res += "\nSession " + str(self.session)
2005-12-03 16:48:10 +00:00
return res + "\n"
def __repr__(self):
return str(self)
def spdl(self):
2005-12-04 18:42:24 +00:00
res = ""
res += "(" + str(self.claimsender)
res += "," + str(self.recipient)
res += ", " + str(self.message)
2005-12-04 18:42:24 +00:00
res += " )"
return res
2005-12-03 16:12:58 +00:00
class State(list):
def __repr__(self):
return "State<" + list.__repr__(self) + ">"
class Label(object):
def __init__(self, name, category):
self.name = name
self.category = category
def __str__(self):
return "lb=" + self.name + ",type=" + self.category
def __repr__(self):
return str(self)
class Rule(object):
2005-12-04 14:46:37 +00:00
def __init__(self,left=[],right=[]):
2005-12-04 16:41:43 +00:00
def sanitize(x):
if x == None:
return []
elif type(x) != list:
return [x]
else:
return x
self.left = sanitize(left)
self.right = sanitize(right)
2005-12-03 16:12:58 +00:00
self.label = None
2005-12-04 16:41:43 +00:00
self.actors = []
2005-12-03 16:12:58 +00:00
def setLabel(self,label):
self.label = label
def __str__(self):
res = "Rule:"
if self.label != None:
res += " (" + str(self.label) +")"
res += "\n"
2005-12-04 14:46:37 +00:00
if len(self.left) > 0:
2005-12-03 16:48:10 +00:00
res += str(self.left) + "\n"
2005-12-04 14:46:37 +00:00
if len(self.right) > 0:
if len(self.left) > 0:
2005-12-03 16:48:10 +00:00
res += "=>\n"
res += str(self.right) + "\n"
res += ".\n"
2005-12-03 16:12:58 +00:00
return res
def __repr__(self):
return str(self)
2005-12-04 16:41:43 +00:00
def getActors(self):
return self.actors
def getFacts(self):
return self.left + self.right
2005-12-04 14:46:37 +00:00
2005-12-03 16:12:58 +00:00
class InitialRule(Rule):
2005-12-04 14:46:37 +00:00
2005-12-03 16:12:58 +00:00
def __str__(self):
return "Initial " + Rule.__str__(self)
2005-12-04 14:46:37 +00:00
2005-12-03 16:12:58 +00:00
class MessageRule(Rule):
2005-12-04 14:46:37 +00:00
def __init__(self,left=[],right=[]):
Rule.__init__(self,left,right)
2005-12-04 16:41:43 +00:00
self.actors = []
# Add actors
2005-12-04 16:41:43 +00:00
for fact in self.getFacts():
2005-12-04 14:46:37 +00:00
actor = fact.getActor()
if actor != None and actor not in self.actors:
2005-12-04 16:41:43 +00:00
self.actors.append(actor)
# Read/Send, before/after
self.readFact = None
self.before = None
for fact in self.left:
if type(fact) == MessageFact:
self.readFact = fact
elif type(fact) == PrincipalFact:
self.before = fact
self.sendFact = None
self.after = None
for fact in self.right:
if type(fact) == MessageFact:
self.sendFact = fact
elif type(fact) == PrincipalFact:
self.after = fact
if self.before == None or self.after == None:
print "Warning: rule does not have both principal facts."
print self
2005-12-04 14:46:37 +00:00
2005-12-03 16:12:58 +00:00
def __str__(self):
return "Message " + Rule.__str__(self)
def getStepFrom(self):
if self.before != None:
return self.before.step
else:
return -1
def getStepTo(self):
if self.after != None:
return self.after.step
else:
return -1
2005-12-03 16:12:58 +00:00
class GoalRule(Rule):
def __str__(self):
return "Goal " + Rule.__str__(self)
class CorrespondenceRule(GoalRule):
def __init__(self, l):
GoalRule.__init__(self,l,None)
def __str__(self):
return "Correspondence " + GoalRule.__str__(self)
class SecrecyRule(GoalRule):
def __init__(self, l):
GoalRule.__init__(self,l,None)
def __str__(self):
return "Secrecy " + GoalRule.__str__(self)
class STSecrecyRule(GoalRule):
def __init__(self, l):
GoalRule.__init__(self,l,None)
def __str__(self):
return "Short-term Secrecy " + GoalRule.__str__(self)
class AuthenticateRule(GoalRule):
def __init__(self, l):
GoalRule.__init__(self,l,None)
def __str__(self):
return "Authenticate " + GoalRule.__str__(self)
2005-12-04 18:42:24 +00:00
class Protocol(list):
def setFilename(self, filename):
2005-12-05 15:51:25 +00:00
self.path = os.path.dirname(filename)
self.filename = os.path.basename(filename)
2005-12-04 18:42:24 +00:00
# Get head of filename (until first dot)
def getBaseName(self):
2005-12-04 18:42:24 +00:00
parts = self.filename.split(".")
if parts[0] == "":
return "None"
else:
return parts[0]
# Construct protocol name from filename
def getName(self):
return self.getBaseName()
2005-12-03 16:12:58 +00:00