- Slow, but seems to work like a charm.
This commit is contained in:
parent
dbc5d62ef6
commit
8f222c9bb7
@ -91,7 +91,11 @@ class Term(object):
|
||||
|
||||
def __str__(self):
|
||||
raise InvalidTerm
|
||||
|
||||
|
||||
# Show more info with simple print
|
||||
def __repr__(self):
|
||||
return "Term("+str(self)+")"
|
||||
|
||||
def constructorTerms(self):
|
||||
raise InvalidTerm
|
||||
|
||||
|
@ -5,8 +5,6 @@ Regarding the AVISPA IF report:
|
||||
|
||||
- Messages do not seem to contain Varable' as an option, seems to be
|
||||
flaw in the BNF.
|
||||
- State has no BNF definition in the second half, it seems.
|
||||
- Is Fact well-defined?
|
||||
- Authenticate has no parameters in it (only constants)
|
||||
STSecrecy
|
||||
matching_request
|
||||
|
@ -149,11 +149,17 @@ def ruleParser ():
|
||||
Witness = Literal("witness") + lbr + Agent + comma + Agent + comma + Constant + comma + Message + rbr
|
||||
Request = Literal("request") + lbr + Agent + comma + Agent + comma + Constant + comma + Message + rbr
|
||||
Authenticate = Literal("request") + lbr + Agent + comma + Agent + comma + Constant + comma + Message + rbr
|
||||
GoalFact = Or ([ Correspondence, Secrecy, STSecrecy, Authenticate ])
|
||||
GoalState = Or ([ Secret, Give, Witness, Request ])
|
||||
GoalState = Or ([ Correspondence, Secrecy, STSecrecy, Authenticate ])
|
||||
GoalFact = Or ([ Secret, Give, Witness, Request ])
|
||||
|
||||
# TimeFact
|
||||
TimeFact = Literal("h") + lbr + Message + rbr
|
||||
|
||||
# Intruder knowledge
|
||||
IntruderKnowledge = Literal("i") + lbr + Message + rbr
|
||||
|
||||
# Facts and states
|
||||
Fact = Or ([ Principal, MessageFact, GoalFact ]) ## Not well defined in BNF
|
||||
Fact = Or ([ Principal, MessageFact, IntruderKnowledge, TimeFact, Secret, Give, Witness, Request ])
|
||||
State = Group(delimitedList (Fact, ".")) ## From initial part of document, not in detailed BNF
|
||||
|
||||
# Rules
|
||||
@ -191,10 +197,21 @@ def ifParser():
|
||||
rulename = Word (alphanums + "_")
|
||||
rulecategory = oneOf("Protocol_Rules Invariant_Rules Decomposition_Rules Intruder_Rules Init Goal")
|
||||
label = hash + Literal("lb") + equal + rulename + comma + Literal("type") + equal + rulecategory
|
||||
labeledrule = Group(label + ruleParser())
|
||||
labeledrule = Group(label) + Group(ruleParser())
|
||||
|
||||
def labeledruleAction(s,l,t):
|
||||
print "-----------------"
|
||||
print "- Detected rule -"
|
||||
print "-----------------"
|
||||
|
||||
print t[0]
|
||||
print t[1]
|
||||
print
|
||||
|
||||
labeledrule.setParseAction(labeledruleAction)
|
||||
|
||||
# A complete file
|
||||
parser = Group(OneOrMore(labeledrule))
|
||||
parser = OneOrMore(labeledrule)
|
||||
parser.ignore("##" + restOfLine)
|
||||
|
||||
return parser
|
||||
@ -217,6 +234,11 @@ def typeSwitch(line):
|
||||
except:
|
||||
print "Unexpected error while determining (un)typedness of the line", line
|
||||
|
||||
str = "Detected "
|
||||
if not typedversion:
|
||||
str += "un"
|
||||
str += "typed version."
|
||||
print str
|
||||
|
||||
# Parse an entire file, including the first one
|
||||
def linesParse(lines):
|
||||
@ -226,9 +248,6 @@ def linesParse(lines):
|
||||
parser = ifParser()
|
||||
result = parser.parseString("".join( lines[1:]))
|
||||
|
||||
for x in result:
|
||||
print x
|
||||
|
||||
# Main code
|
||||
def main():
|
||||
file = open("NSPK_LOWE.if", "r")
|
||||
|
Loading…
Reference in New Issue
Block a user