diff --git a/scripts/if2spdl/Term.py b/scripts/if2spdl/Term.py index 5dbde34..c4fdc4d 100644 --- a/scripts/if2spdl/Term.py +++ b/scripts/if2spdl/Term.py @@ -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 diff --git a/scripts/if2spdl/notes.txt b/scripts/if2spdl/notes.txt index aad128c..80bd335 100644 --- a/scripts/if2spdl/notes.txt +++ b/scripts/if2spdl/notes.txt @@ -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 diff --git a/scripts/if2spdl/parser.py b/scripts/if2spdl/parser.py index 3f7865b..9cff2a7 100755 --- a/scripts/if2spdl/parser.py +++ b/scripts/if2spdl/parser.py @@ -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")