- Added Gijs' stuff.
This commit is contained in:
ccremers
parent
58f3aafc65
commit
60d6a10b04
204
scripts/if2spdl/Term.py
Normal file
204
scripts/if2spdl/Term.py
Normal file
|
|
@ -0,0 +1,204 @@
|
|||
#
|
||||
# Term
|
||||
#
|
||||
import Trace
|
||||
from misc import *
|
||||
|
||||
class InvalidTerm(TypeError):
|
||||
"Exception used to indicate that a given term is invalid"
|
||||
|
||||
|
||||
class Knowledge(object):
|
||||
def __init__(self,attack):
|
||||
self.attack = attack
|
||||
self.knowledge = []
|
||||
|
||||
def getInverse(self,term):
|
||||
for pair in self.attack.inverseKeys:
|
||||
if term == pair[0]:
|
||||
return pair[1]
|
||||
if term == pair[1]:
|
||||
return pair[0]
|
||||
|
||||
# Get the inverse key
|
||||
def getInverseKey(self,term):
|
||||
# First try to see if the entire term has an inverse
|
||||
result = self.getInverse(term)
|
||||
if result != None:
|
||||
return result
|
||||
|
||||
# If it is an apply term, try to see if the function has an inverse
|
||||
if isinstance(term,TermApply):
|
||||
result = self.getInverse(term.function)
|
||||
if result != None:
|
||||
return TermApply(result,term.argument)
|
||||
|
||||
# No inverse found, so term is its own inverse
|
||||
return term
|
||||
|
||||
# Add a term to the knowledge
|
||||
def add(self,term):
|
||||
if term == None:
|
||||
return
|
||||
added = False
|
||||
for x in term.deriveTerms(self):
|
||||
if not x in self.knowledge:
|
||||
added = True
|
||||
self.knowledge.append(x)
|
||||
|
||||
# Something new was added, maybe this can help us to decrypt a term
|
||||
# that we could not decrypt before
|
||||
if added:
|
||||
for x in self.knowledge:
|
||||
if isinstance(x,TermEncrypt):
|
||||
self.add(x)
|
||||
|
||||
def canDerive(self,term):
|
||||
# We can derive free variables, because we can even choose them
|
||||
if isinstance(term,TermVariable) and term.isFree():
|
||||
return True
|
||||
# We can derive a term if it is in the knowledge
|
||||
# or all terms required to construct it are in the knowledge
|
||||
if exists(lambda x: x == term,self.knowledge):
|
||||
return True
|
||||
constructors = term.constructorTerms()
|
||||
|
||||
if len(constructors) == 1 and constructors[0] == term:
|
||||
# This is a single term, there is no need to look at constructor
|
||||
# terms as we have already looked at the complete term
|
||||
return False
|
||||
|
||||
return forall(lambda x: self.canDerive(x),constructors)
|
||||
|
||||
|
||||
# Knowledge is the initial knowledge and all messages in sends
|
||||
def buildKnowledge(self):
|
||||
self.knowledge = self.attack.initialKnowledge[:]
|
||||
for run in self.attack.semiTrace.runs:
|
||||
# Intruder actions do not add knowledge processing them
|
||||
# is a waste of time
|
||||
if run.intruder:
|
||||
continue
|
||||
for event in run:
|
||||
if isinstance(event,Trace.EventSend):
|
||||
self.add(event.message)
|
||||
self.add(event.fr)
|
||||
self.add(event.to)
|
||||
|
||||
class Term(object):
|
||||
def __init__(self):
|
||||
self.types = None
|
||||
|
||||
def __str__(self):
|
||||
raise InvalidTerm
|
||||
|
||||
def constructorTerms(self):
|
||||
raise InvalidTerm
|
||||
|
||||
def deriveTerms(self,knowledge):
|
||||
raise InvalidTerm
|
||||
|
||||
# Two terms are equal when their string rep is equal
|
||||
def __cmp__(self,other):
|
||||
return cmp(str(self),str(other))
|
||||
|
||||
|
||||
class TermConstant(Term):
|
||||
def __init__(self, constant):
|
||||
Term.__init__(self)
|
||||
self.value = str(constant)
|
||||
|
||||
def deriveTerms(self,knowledge):
|
||||
return [self]
|
||||
|
||||
def constructorTerms(self):
|
||||
return [self]
|
||||
|
||||
def __str__(self):
|
||||
return self.value
|
||||
|
||||
class TermEncrypt(Term):
|
||||
def __init__(self, value, key):
|
||||
Term.__init__(self)
|
||||
self.value = value
|
||||
self.key = key
|
||||
|
||||
def deriveTerms(self,knowledge):
|
||||
# In order to unpack an encrypted term we have to have the inverse key
|
||||
inverse = knowledge.getInverseKey(self.key)
|
||||
if knowledge.canDerive(inverse):
|
||||
return [self] + [self.value] + self.value.deriveTerms(knowledge)
|
||||
else:
|
||||
return [self]
|
||||
|
||||
def constructorTerms(self):
|
||||
return [self.value,self.key]
|
||||
|
||||
def __str__(self):
|
||||
return "{%s}%s" % (self.value, self.key)
|
||||
|
||||
class TermApply(Term):
|
||||
def __init__(self, function, argument):
|
||||
Term.__init__(self)
|
||||
self.function = function
|
||||
self.argument = argument
|
||||
|
||||
def constructorTerms(self):
|
||||
return [self.function,self.argument]
|
||||
|
||||
def deriveTerms(self,knowledge):
|
||||
return [self]
|
||||
|
||||
def __str__(self):
|
||||
return "%s(%s)" % (self.function, self.argument)
|
||||
|
||||
class TermVariable(Term):
|
||||
def __init__(self, name, value):
|
||||
Term.__init__(self)
|
||||
self.name = name
|
||||
self.value = value
|
||||
|
||||
def isFree(self):
|
||||
return self.value == None
|
||||
|
||||
def constructorTerms(self):
|
||||
if self.value != None:
|
||||
return [self.value]
|
||||
else:
|
||||
return [self.name]
|
||||
|
||||
def deriveTerms(self,knowledge):
|
||||
if self.value != None:
|
||||
return [self,self.value] + self.value.deriveTerms(knowledge)
|
||||
else:
|
||||
return [self,self.name]
|
||||
|
||||
def __str__(self):
|
||||
if (self.value != None):
|
||||
return str(self.value)
|
||||
else:
|
||||
return str(self.name)
|
||||
|
||||
class TermTuple(Term):
|
||||
def __init__(self, op1, op2):
|
||||
Term.__init__(self)
|
||||
self.op1 = op1
|
||||
self.op2 = op2
|
||||
|
||||
def __str__(self):
|
||||
return "%s,%s" % (self.op1,self.op2)
|
||||
|
||||
def constructorTerms(self):
|
||||
return [self.op1,self.op2]
|
||||
|
||||
def deriveTerms(self,knowledge):
|
||||
return [self,self.op1,self.op2]+self.op1.deriveTerms(knowledge)+self.op2.deriveTerms(knowledge)
|
||||
|
||||
def __getitem__(self,index):
|
||||
if index == 0:
|
||||
return self.op1
|
||||
elif index == 1:
|
||||
return self.op2
|
||||
else:
|
||||
return self.op2.__getitem__(index-1)
|
||||
|
||||
297
scripts/if2spdl/Trace.py
Normal file
297
scripts/if2spdl/Trace.py
Normal file
|
|
@ -0,0 +1,297 @@
|
|||
#
|
||||
# Trace
|
||||
#
|
||||
from misc import *
|
||||
|
||||
class InvalidAction(TypeError):
|
||||
"Exception used to indicate that a given action is invalid"
|
||||
|
||||
class InvalidEvent(TypeError):
|
||||
"Exception used to indicate that a given event is invalid"
|
||||
|
||||
class SemiTrace(object):
|
||||
def __init__(self):
|
||||
self.runs = []
|
||||
|
||||
def totalCount(self):
|
||||
count = 0
|
||||
for run in self.runs:
|
||||
count += len(run.eventList)
|
||||
return count
|
||||
|
||||
def sortActions(self,actionlist):
|
||||
newlist = actionlist[:]
|
||||
newlist.sort(lambda x,y: self.getOrder(x,y))
|
||||
return newlist
|
||||
|
||||
def getEnabled(self,previous):
|
||||
enabled = []
|
||||
for run in self.runs:
|
||||
for event in run:
|
||||
if event in previous or event in enabled:
|
||||
continue
|
||||
prec = self.getPrecedingEvents(event,previous)
|
||||
if len(prec) == 0:
|
||||
enabled.append(event)
|
||||
return enabled
|
||||
|
||||
# Returns run,index tuples for all connections
|
||||
def getConnections(self,event,removeIntruder=False):
|
||||
if not removeIntruder:
|
||||
return event.follows
|
||||
result = []
|
||||
if event.run.intruder:
|
||||
for before in event.getBefore():
|
||||
result.extend(self.getConnections(before,removeIntruder))
|
||||
|
||||
for x in event.follows:
|
||||
fol = self.getEvent(x)
|
||||
# If this is an intruder action descend into it
|
||||
if fol.run.intruder:
|
||||
result.extend(self.getConnections(fol,removeIntruder))
|
||||
else:
|
||||
result.append(x)
|
||||
return uniq(result)
|
||||
|
||||
# Return the minimum set of preceding events for a given event
|
||||
# that is the events before this event in the same run and all
|
||||
# actions required by the partional ordering
|
||||
# If previous is non empty remove all events already in previous
|
||||
def getPrecedingEvents(self,event,previous=[]):
|
||||
# If it is cached return cached version
|
||||
if event.preceding != None:
|
||||
return filter(lambda x: x not in previous,event.preceding)
|
||||
preceding = []
|
||||
for prec in event.getBefore():
|
||||
preceding.append(prec)
|
||||
preceding.extend(self.getPrecedingEvents(prec))
|
||||
for x in event.follows:
|
||||
fol = self.getEvent(x)
|
||||
preceding.append(fol)
|
||||
preceding.extend(self.getPrecedingEvents(fol))
|
||||
preceding = uniq(preceding)
|
||||
event.preceding = preceding
|
||||
preceding = filter(lambda x: x not in previous,preceding)
|
||||
return preceding
|
||||
|
||||
# Returns -1 if the first event has to be before the second one
|
||||
# +1 if the second event has to be before the first one
|
||||
# 0 if there is no order defined on the two events
|
||||
def getOrder(self,event1,event2):
|
||||
if (event1 in self.getPrecedingEvents(event2)):
|
||||
return -1
|
||||
if (event2 in self.getPrecedingEvents(event1)):
|
||||
return 1
|
||||
return 0
|
||||
|
||||
# Get event by run id and index
|
||||
def getEvent(self,idx):
|
||||
(rid,index) = idx
|
||||
for run in self.runs:
|
||||
if run.id != rid:
|
||||
continue
|
||||
for event in run:
|
||||
if event.index == index:
|
||||
return event
|
||||
raise InvalidEvent
|
||||
|
||||
# Get all claim events in the trace
|
||||
def getClaims(self):
|
||||
claims = []
|
||||
for run in self.runs:
|
||||
for event in run:
|
||||
if isinstance(event,EventClaim):
|
||||
claims.append(event)
|
||||
return claims
|
||||
|
||||
# Returns a list of all initiation events in the semitrace
|
||||
def getInitiations(self):
|
||||
initiations = []
|
||||
for run in self.runs:
|
||||
# Initiations are runs of honest agents
|
||||
if (run.intruder):
|
||||
continue
|
||||
# Which contain no reads before the first send
|
||||
for action in run:
|
||||
if (isinstance(action,EventRead)):
|
||||
break
|
||||
elif (isinstance(action,EventSend)):
|
||||
initiations.append(action)
|
||||
break
|
||||
return initiations
|
||||
|
||||
# Get all runs performed by a specific agent
|
||||
def getAgentRuns(self,agent):
|
||||
result = []
|
||||
for run in self.runs:
|
||||
if run.getAgent() == agent:
|
||||
result.append(run)
|
||||
return result
|
||||
|
||||
# Return a list of all runs that are parallel with this run
|
||||
def getParallelRuns(self,run):
|
||||
parallel = []
|
||||
first = run.getFirstAction()
|
||||
# Process all events that are before the end of the run
|
||||
for event in self.getPrecedingEvents(run.getLastAction()):
|
||||
# Only count those we haven't found yet
|
||||
if event.run in parallel or event.run == run:
|
||||
continue
|
||||
# If the event is also after the beginning of the run it is
|
||||
# parallel
|
||||
if self.getOrder(event,first) == 1:
|
||||
parallel.append(event.run)
|
||||
return parallel
|
||||
|
||||
class ProtocolDescription(object):
|
||||
def __init__(self,protocol):
|
||||
self.protocol = protocol
|
||||
self.roledescr = {}
|
||||
|
||||
# Find event by label
|
||||
def findEvent(self,eventlabel,eventType=None):
|
||||
for (role,descr) in self.roledescr.items():
|
||||
for event in descr:
|
||||
if event.label == eventlabel:
|
||||
if eventType == None or isinstance(event,eventType):
|
||||
return event
|
||||
|
||||
# Return all events that should have occured before the given event
|
||||
# if the protocol is executed exactly as specified
|
||||
# (i.e. all previous events in the same run and the preceding events
|
||||
# of the matching sends of all reads)
|
||||
def getPrecedingEvents(self,eventlabel,eventType=None):
|
||||
event = self.findEvent(eventlabel,eventType)
|
||||
if event.preceding != None:
|
||||
return event.preceding
|
||||
preceding = event.getBefore()+[event]
|
||||
for prev in preceding:
|
||||
# For this event and all events that are before it in the run
|
||||
# description see if it is a read and if it is also add the
|
||||
# precedinglabelset of the matching send
|
||||
if (isinstance(prev,EventRead)):
|
||||
match = self.findEvent(prev.label,EventSend)
|
||||
if match:
|
||||
preceding.extend(self.getPrecedingEvents(match.label,EventSend))
|
||||
preceding = uniq(preceding)
|
||||
event.preceding = preceding
|
||||
return preceding
|
||||
|
||||
# Calculate the preceding labelset that is all read events
|
||||
# that are in the precedingEvents of a certain event
|
||||
def getPrecedingLabelSet(self,eventlabel):
|
||||
events = self.getPrecedingEvents(eventlabel)
|
||||
events = filter(lambda x: isinstance(x,EventRead),events)
|
||||
return [x.label for x in events]
|
||||
|
||||
# Calculate the roles in preceding labelset that is all roles that
|
||||
# that are in the precedingEvents of a certain event
|
||||
def getPrecedingRoleSet(self,eventlabel):
|
||||
events = self.getPrecedingEvents(eventlabel)
|
||||
roles = uniq([x.run.role for x in events])
|
||||
return roles
|
||||
|
||||
|
||||
def __str__(self):
|
||||
s = ''
|
||||
for x in self.roledescr.values():
|
||||
for e in x:
|
||||
s += str(e) + "\n"
|
||||
return s
|
||||
|
||||
class Run(object):
|
||||
def __init__(self):
|
||||
self.id = None
|
||||
self.protocol = None
|
||||
self.role = None
|
||||
self.roleAgents = {}
|
||||
self.eventList = []
|
||||
self.intruder = False
|
||||
self.attack = None
|
||||
|
||||
def __iter__(self):
|
||||
return iter(self.eventList)
|
||||
|
||||
def getAgent(self):
|
||||
if self.intruder:
|
||||
return None
|
||||
return self.roleAgents[self.role]
|
||||
|
||||
def getFirstAction(self):
|
||||
return self.eventList[0]
|
||||
|
||||
def getLastAction(self):
|
||||
return self.eventList[-1]
|
||||
|
||||
class Event(object):
|
||||
def __init__(self,index,label,follows):
|
||||
self.index = index
|
||||
self.label = label
|
||||
self.follows = follows
|
||||
self.run = None
|
||||
self.preceding = None
|
||||
self.rank = None
|
||||
|
||||
def getBefore(self):
|
||||
result = []
|
||||
for event in self.run:
|
||||
if (event == self):
|
||||
return result
|
||||
result.append(event)
|
||||
# This should never happen
|
||||
assert(False)
|
||||
|
||||
class EventSend(Event):
|
||||
def __init__(self,index,label,follows,fr,to,message):
|
||||
Event.__init__(self,index,label,follows)
|
||||
self.fr = fr
|
||||
self.to = to
|
||||
self.message = message
|
||||
|
||||
def __str__(self):
|
||||
if self.run.intruder:
|
||||
return "SEND(%s)" % self.message
|
||||
else:
|
||||
return "SEND_%s(%s,%s)" % (self.label[1],self.to,self.message)
|
||||
|
||||
class EventRead(Event):
|
||||
def __init__(self,index,label,follows,fr,to,message):
|
||||
Event.__init__(self,index,label,follows)
|
||||
self.fr = fr
|
||||
self.to = to
|
||||
self.message = message
|
||||
|
||||
def __str__(self):
|
||||
if self.run.intruder:
|
||||
return "READ(%s)" % self.message
|
||||
else:
|
||||
return "READ_%s(%s,%s)" % (self.label[1],self.fr, self.message)
|
||||
|
||||
class EventClaim(Event):
|
||||
def __init__(self,index,label,follows,role,type,argument):
|
||||
Event.__init__(self,index,label,follows)
|
||||
self.role = role
|
||||
self.type = type
|
||||
self.argument = argument
|
||||
self.broken = None
|
||||
|
||||
# A Claim should be ignored if there is an untrusted agent in the role
|
||||
# agents
|
||||
def ignore(self):
|
||||
for untrusted in self.run.attack.untrusted:
|
||||
if untrusted in self.run.roleAgents.values():
|
||||
return True
|
||||
return False
|
||||
|
||||
# Return (protocol,role)
|
||||
def protocolRole(self):
|
||||
return "(%s,%s)" % (self.run.protocol,self.run.role)
|
||||
|
||||
def argstr(self):
|
||||
if self.argument == None:
|
||||
return '*'
|
||||
else:
|
||||
return str(self.argument)
|
||||
|
||||
def __str__(self):
|
||||
return "CLAIM_%s(%s, %s)" % (self.label[1],self.type,self.argstr())
|
||||
|
|
@ -1,16 +1,33 @@
|
|||
#!/usr/bin/python
|
||||
|
||||
import pprint
|
||||
|
||||
def unfold(arg):
|
||||
for x in arg:
|
||||
print x
|
||||
pprint.pprint(x)
|
||||
|
||||
def intruderKnowledge(x):
|
||||
print "Intruder knowledge"
|
||||
unfold(x)
|
||||
|
||||
def scenario(x):
|
||||
print "Scenario",x,"ignoring for now"
|
||||
|
||||
def initialState(arg):
|
||||
arg = arg[0] # One level deeper (has no implication rule)
|
||||
print "Initial State"
|
||||
unfold(arg)
|
||||
print len(arg)
|
||||
for x in arg:
|
||||
if x[0] == "h":
|
||||
print "Some stupid semi time thing"
|
||||
if x[0] == "i":
|
||||
intruderKnowledge(x),"ignoring for now"
|
||||
elif x[0] == "w":
|
||||
scenario(x)
|
||||
|
||||
# Ignore for now
|
||||
def protocolRules(arg):
|
||||
print "Protocol Rules"
|
||||
unfold(arg)
|
||||
return
|
||||
|
||||
# Goals: ignored for now
|
||||
def goal(arg):
|
||||
|
|
|
|||
29
scripts/if2spdl/misc.py
Normal file
29
scripts/if2spdl/misc.py
Normal file
|
|
@ -0,0 +1,29 @@
|
|||
#
|
||||
# misc.py
|
||||
# Various helper functions
|
||||
|
||||
def confirm(question):
|
||||
answer = ''
|
||||
while answer not in ('y','n'):
|
||||
print question,
|
||||
answer = raw_input().lower()
|
||||
return answer == 'y'
|
||||
|
||||
def exists(func,list):
|
||||
return len(filter(func,list)) > 0
|
||||
|
||||
def forall(func,list):
|
||||
return len(filter(func,list)) == len(list)
|
||||
|
||||
def uniq(li):
|
||||
result = []
|
||||
for elem in li:
|
||||
if (not elem in result):
|
||||
result.append(elem)
|
||||
return result
|
||||
|
||||
# Return a sorted copy of a list
|
||||
def sorted(li):
|
||||
result = li[:]
|
||||
result.sort()
|
||||
return result
|
||||
|
|
@ -6,6 +6,7 @@
|
|||
from pyparsing import Word, alphanums, alphas, nums, oneOf, restOfLine, OneOrMore, \
|
||||
ParseResults, Forward, Combine, Or, Optional,MatchFirst, \
|
||||
ZeroOrMore, StringEnd, LineEnd, delimitedList, Group, Literal
|
||||
import Term
|
||||
|
||||
def ifParse (str):
|
||||
# Tokens
|
||||
|
|
@ -38,18 +39,21 @@ def ifParse (str):
|
|||
|
||||
# Message section
|
||||
Alfabet= alphas+nums+"_$"
|
||||
Variable = Word("x",Alfabet).setName("variable")
|
||||
Constant = Word(alphas,Alfabet).setName("constant")
|
||||
Number = Word(nums).setName("number")
|
||||
Variable = Word("x",Alfabet).setParseAction(lambda s,l,t: [ Term.TermVariable(t[0],None) ])
|
||||
Constant = Word(alphas,Alfabet).setParseAction(lambda s,l,t: [ Term.TermConstant(t[0]) ])
|
||||
Number = Word(nums).setParseAction(lambda s,l,t: [ Term.TermConstant(t[0]) ])
|
||||
|
||||
Basic = MatchFirst([ Variable, Constant, Number ])
|
||||
|
||||
Message = Forward()
|
||||
TypeInfo = oneOf ("mr nonce pk sk fu table")
|
||||
TypeMsg = Group(TypeInfo + lbr + Message + rbr).setName("typeinfo")
|
||||
TypeInfo = oneOf ("mr nonce pk sk fu table").setParseAction(lambda s,l,t: [ Term.TermConstant(t[0]) ])
|
||||
TypeMsg = Group(TypeInfo + lbr + Message + rbr).setParseAction(lambda s,l,t: [ t[3].setType(t[1]) ])
|
||||
|
||||
CryptOp = oneOf ("crypt scrypt c funct rcrypt tb")
|
||||
CryptMsg = Group(CryptOp + lbr + Message + com + Message + rbr).setName("crypt")
|
||||
SMsg = Group(Literal("s") + lbr + Message + rbr)
|
||||
Message << Or ([TypeMsg, CryptMsg, SMsg, Basic]) + Optional(Literal("'"))
|
||||
Message << Group(Or ([TypeMsg, CryptMsg, SMsg, Basic]) +
|
||||
Optional(Literal("'")) )
|
||||
|
||||
# Fact section
|
||||
Request = Group("request" + btup(4))
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user