From 2fe91a2eb17f4ad0f968e6df66612b44b3e0ccdb Mon Sep 17 00:00:00 2001 From: ccremers Date: Wed, 16 Nov 2005 16:24:18 +0000 Subject: [PATCH] - Made a start with if2spdl parser. --- scripts/if2spdl/parser.py | 86 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 86 insertions(+) create mode 100755 scripts/if2spdl/parser.py diff --git a/scripts/if2spdl/parser.py b/scripts/if2spdl/parser.py new file mode 100755 index 0000000..04278cb --- /dev/null +++ b/scripts/if2spdl/parser.py @@ -0,0 +1,86 @@ +#!/usr/bin/python + +# requires python-pyparsing module +# http://pyparsing.sourceforge.net/ + +from pyparsing import Word, alphanums, alphas, nums, oneOf, restOfLine, OneOrMore, \ + ParseResults, Forward, Combine, Or, Optional,MatchFirst, \ + ZeroOrMore, StringEnd, LineEnd, delimitedList, Group, Literal + +def parse (str): + # Tokens + lbr = Literal("(").suppress() + rbr = Literal(")").suppress() + com = Literal(",").suppress() + + # Functions to construct tuples etc + def bracket(x): + return lbr + x + rbr + + def ntup(n): + x = Message + while n > 1: + x = x + com + Message + n = n - 1 + return x + + def btup(n): + return bracket(ntup(n)) + + def funcy(x,y): + return x + bracket(y) + + def ftup(x,n): + return funcy(x, ntup(n)) + + # Message section + Alfabet= alphas+nums+"_$" + Variable = Word("x",Alfabet) + Constant = Word(alphas,Alfabet) + Number = Word(nums) + Basic = MatchFirst([ Variable, Constant, Number ]) + + Message = Forward() + TypeInfo = oneOf ("mr nonce pk sk fu table") + TypeMsg = TypeInfo + lbr + Message + rbr + CryptOp = oneOf ("crypt scrypt c funct rcrypt tb") + CryptMsg = CryptOp + lbr + Message + com + Message + rbr + SMsg = Literal("s") + lbr + Message + rbr + Message << Or ([TypeMsg, CryptMsg, SMsg, Basic]) + Optional(Literal("'")) + + # Fact section + + Request = "request" + btup(4) + Witness = "witness" + btup(4) + Give = "give" + lbr + Message + com + ftup(Literal("f"), 1) + rbr + Secret = "secret" + lbr + Message + com + ftup(Literal("f"),1) + rbr + TimeFact = ftup (Literal("h"), 1) + IntruderKnowledge = ftup (Literal("i"), 1) + MessageFact = ftup(Literal("m"),6) + Principal = ftup(Literal("w"), 7) + + Fact = Principal | MessageFact | IntruderKnowledge | TimeFact | Secret | Give | Witness | Request + + #State = Fact + OptioZeroOrMore ("." + Fact) + State = delimitedList (Fact, ".") + + # Rules and labels + rulename = Word (alphanums + "_") + rulecategory = oneOf("Protocol_Rules Invariant_Rules Decomposition_Rules Intruder_Rules Init Goal") + label = "# lb=" + rulename + "," + "type=" + rulecategory + rule = State + Optional("\n" + "=>" + "\n" + State) + labeledrule = Group(label + rule) + typeflag = "# option=" + oneOf ("untyped","typed") + + # A complete file + iffile = typeflag + OneOrMore(labeledrule) + + parser = iffile + parser.ignore("##" + restOfLine) + + return parser.parseString(str) + +file = open("NSPK_LOWE.if", "r") +res = parse ("".join(file.readlines() ) ) +print res +