From 9e5a076d7d9c12bf5cf64ba1c0475685722e5b3e Mon Sep 17 00:00:00 2001 From: ccremers Date: Wed, 16 Nov 2005 16:44:56 +0000 Subject: [PATCH] - Added test file. - Created main file. --- scripts/if2spdl/NSPK_LOWE.if | 54 ++++++++++++++++++++++++++++++++++++ scripts/if2spdl/if2spdl.py | 14 ++++++++++ scripts/if2spdl/parser.py | 45 +++++++++++++++--------------- 3 files changed, 91 insertions(+), 22 deletions(-) create mode 100644 scripts/if2spdl/NSPK_LOWE.if create mode 100755 scripts/if2spdl/if2spdl.py diff --git a/scripts/if2spdl/NSPK_LOWE.if b/scripts/if2spdl/NSPK_LOWE.if new file mode 100644 index 0000000..f66e7cf --- /dev/null +++ b/scripts/if2spdl/NSPK_LOWE.if @@ -0,0 +1,54 @@ +# option=untyped +# lb=Step_0, type=Protocol_Rules +h(s(xTime)).w(0,mr(I),xA,etc,c(xA,c(xB,c(xKa,c(xKa',c(xKb,etc))))),true,xc) +=> +h(xTime).m(1,xA,xA,xB,crypt(xKb,c(nonce(c(Na,xTime)),xA)),xc).w(2,xB,xA,c(nonce(c(Na,xTime)),etc),c(xA,c(xB,c(xKa,c(xKa',c(xKb,etc))))),true,xc).witness(xA,xB,Na,nonce(c(Na,xTime))) + + +# lb=Step_1, type=Protocol_Rules +h(s(xTime)).m(1,xr,xA,xB,crypt(xKb,c(xNa,xA)),xc2).w(1,xA,xB,etc,c(xA,c(xB,c(xKa,c(xKb,c(xKb',etc))))),xbool,xc) +=> +h(xTime).m(2,xB,xB,xA,crypt(xKa,c(c(xNa,nonce(c(Nb,xTime))),xB)),xc2).w(3,xA,xB,c(crypt(xKb,c(xNa,xA)),c(nonce(c(Nb,xTime)),etc)),c(xA,c(xB,c(xKa,c(xKb,c(xKb',etc))))),true,xc).witness(xB,xA,Nb,nonce(c(Nb,xTime))) + + +# lb=Step_2, type=Protocol_Rules +h(s(xTime)).m(2,xr,xB,xA,crypt(xKa,c(c(xNa,xNb),xB)),xc2).w(2,xB,xA,c(xNa,etc),c(xA,c(xB,c(xKa,c(xKa',c(xKb,etc))))),xbool,xc) +=> +h(xTime).m(3,xA,xA,xB,crypt(xKb,xNb),xc2).w(0,mr(I),xA,etc,c(xA,c(xB,c(xKa,c(xKa',c(xKb,etc))))),true,s(xc)).request(xA,xB,Nb,xNb) + + +# lb=Step_3, type=Protocol_Rules +h(s(xTime)).m(3,xr,xA,xB,crypt(xKb,xNb),xc2).w(3,xA,xB,c(crypt(xKb,c(xNa,xA)),c(xNb,etc)),c(xA,c(xB,c(xKa,c(xKb,c(xKb',etc))))),xbool,xc) +=> +h(xTime).w(1,xA,xB,etc,c(xA,c(xB,c(xKa,c(xKb,c(xKb',etc))))),true,s(xc)).request(xB,xA,Na,xNa) + + + +# lb=Initial_state, type=Init +h(xTime).w(1,mr(I),mr(a),etc,c(mr(I),c(mr(a),c(pk(ki),c(pk(ka),c(pk(ka)',etc))))),true,2).w(1,mr(a),mr(b),etc,c(mr(a),c(mr(b),c(pk(ka),c(pk(kb),c(pk(kb)',etc))))),true,1).w(0,mr(I),mr(a),etc,c(mr(a),c(mr(b),c(pk(ka),c(pk(ka)',c(pk(kb),etc))))),true,1).i(mr(I)).i(mr(b)).i(pk(ka)).i(pk(kb)).i(pk(ki)).i(nonce(c(ni,ni))).i(sk(c(ni,ni))).i(pk(c(ni,ni))).i(pk(c(ni,ni))').i(mr(a)).i(pk(ki)') +# lb=Authenticate_a_I_7, type=Goal +request(mr(a),mr(I),x1,x2) + +# lb=Authenticate_a_a_6, type=Goal +request(mr(a),mr(a),x1,x2) + +# lb=Authenticate_b_I_5, type=Goal +request(mr(b),mr(I),x1,x2) + +# lb=Authenticate_b_a_4, type=Goal +request(mr(b),mr(a),x1,x2) + +# lb=Authenticate_I_a_3, type=Goal +request(mr(I),mr(a),x1,x2) + +# lb=Authenticate_I_b_2, type=Goal +request(mr(I),mr(b),x1,x2) + +# lb=Authenticate_a_a_1, type=Goal +request(mr(a),mr(a),x1,x2) + +# lb=Authenticate_a_b_0, type=Goal +request(mr(a),mr(b),x1,x2) + + + diff --git a/scripts/if2spdl/if2spdl.py b/scripts/if2spdl/if2spdl.py new file mode 100755 index 0000000..0b95712 --- /dev/null +++ b/scripts/if2spdl/if2spdl.py @@ -0,0 +1,14 @@ +#!/usr/bin/python + +from parser import * +import pprint + +def main(): + file = open("NSPK_LOWE.if", "r") + res = ifParse ("".join(file.readlines() ) ) + pprint.pprint (res.asList()) + + + +if __name__ == "__main__": + main() diff --git a/scripts/if2spdl/parser.py b/scripts/if2spdl/parser.py index 04278cb..2e0cc13 100755 --- a/scripts/if2spdl/parser.py +++ b/scripts/if2spdl/parser.py @@ -7,11 +7,14 @@ from pyparsing import Word, alphanums, alphas, nums, oneOf, restOfLine, OneOrMor ParseResults, Forward, Combine, Or, Optional,MatchFirst, \ ZeroOrMore, StringEnd, LineEnd, delimitedList, Group, Literal -def parse (str): +def ifParse (str): # Tokens lbr = Literal("(").suppress() rbr = Literal(")").suppress() com = Literal(",").suppress() + hash = Literal("#").suppress() + equ = Literal("=").suppress() + implies = Literal("=>").suppress() # Functions to construct tuples etc def bracket(x): @@ -35,29 +38,30 @@ def parse (str): # Message section Alfabet= alphas+nums+"_$" - Variable = Word("x",Alfabet) - Constant = Word(alphas,Alfabet) - Number = Word(nums) + Variable = Word("x",Alfabet).setName("variable") + Constant = Word(alphas,Alfabet).setName("constant") + Number = Word(nums).setName("number") Basic = MatchFirst([ Variable, Constant, Number ]) Message = Forward() TypeInfo = oneOf ("mr nonce pk sk fu table") - TypeMsg = TypeInfo + lbr + Message + rbr + TypeMsg = Group(TypeInfo + lbr + Message + rbr).setName("typeinfo") CryptOp = oneOf ("crypt scrypt c funct rcrypt tb") - CryptMsg = CryptOp + lbr + Message + com + Message + rbr - SMsg = Literal("s") + lbr + Message + rbr + 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("'")) # 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) + Request = Group("request" + btup(4)) + Witness = Group("witness" + btup(4)) + Give = Group("give" + lbr + Message + com + ftup(Literal("f"), + 1) + rbr) + Secret = Group("secret" + lbr + Message + com + + ftup(Literal("f"),1) + rbr) + TimeFact = Group(ftup (Literal("h"), 1)) + IntruderKnowledge = Group(ftup (Literal("i"), 1)) + MessageFact = Group(ftup(Literal("m"),6)) + Principal = Group(ftup(Literal("w"), 7)) Fact = Principal | MessageFact | IntruderKnowledge | TimeFact | Secret | Give | Witness | Request @@ -67,10 +71,10 @@ def parse (str): # 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) + label = hash + "lb" + equ + rulename + com + "type" + equ + rulecategory + rule = State + Optional(implies + State) labeledrule = Group(label + rule) - typeflag = "# option=" + oneOf ("untyped","typed") + typeflag = hash + "option" + equ + oneOf ("untyped","typed") # A complete file iffile = typeflag + OneOrMore(labeledrule) @@ -80,7 +84,4 @@ def parse (str): return parser.parseString(str) -file = open("NSPK_LOWE.if", "r") -res = parse ("".join(file.readlines() ) ) -print res