From b436d4923a2e1a02443d5202dc2e88c7b15d1abe Mon Sep 17 00:00:00 2001 From: ccremers Date: Wed, 16 Nov 2005 19:37:42 +0000 Subject: [PATCH] - Starting to get better, almost got terms out of initial knowledge. --- scripts/if2spdl/generator.py | 2 +- scripts/if2spdl/parser.py | 26 ++++++++++++++++++++++---- 2 files changed, 23 insertions(+), 5 deletions(-) diff --git a/scripts/if2spdl/generator.py b/scripts/if2spdl/generator.py index 7ecf12c..47c9a60 100644 --- a/scripts/if2spdl/generator.py +++ b/scripts/if2spdl/generator.py @@ -8,7 +8,7 @@ def unfold(arg): def intruderKnowledge(x): print "Intruder knowledge" - unfold(x) + print x[0], str(x[1]) def scenario(x): print "Scenario",x,"ignoring for now" diff --git a/scripts/if2spdl/parser.py b/scripts/if2spdl/parser.py index 80b0549..e2febea 100755 --- a/scripts/if2spdl/parser.py +++ b/scripts/if2spdl/parser.py @@ -46,14 +46,32 @@ def ifParse (str): Basic = MatchFirst([ Variable, Constant, Number ]) Message = Forward() + + def parseType(s,l,t): + term = t[0][1] + term.setType(t[0][0]) + return [term] + 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]) ]) + TypeMsg = Group(TypeInfo + lbr + Message + rbr).setParseAction(parseType) + + def parseCrypt(s,l,t): + # Crypto types are ignored for now + return [Term.TermEncrypt(t[0][2],t[0][1])] CryptOp = oneOf ("crypt scrypt c funct rcrypt tb") - CryptMsg = Group(CryptOp + lbr + Message + com + Message + rbr).setName("crypt") + CryptMsg = Group(CryptOp + lbr + Message + com + Message + rbr).setParseAction(parseCrypt) + + def parseSMsg(s,l,t): + return [Term.TermEncrypt(t[0][1],Term.Termconstant("succ") )] + SMsg = Group(Literal("s") + lbr + Message + rbr) - Message << Group(Or ([TypeMsg, CryptMsg, SMsg, Basic]) + - Optional(Literal("'")) ) + + def parsePrime(s,l,t): + # for now, we simply ignore the prime (') + return [t[0][0]] + + Message << Group(Or ([TypeMsg, CryptMsg, SMsg, Basic]) + Optional(Literal("'"))).setParseAction(parsePrime) # Fact section Request = Group("request" + btup(4))