- Added test file.

- Created main file.

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)
+
+
+

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()

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)
+	Variable = Word("x",Alfabet).setName("variable")
-	Constant = Word(alphas,Alfabet)
+	Constant = Word(alphas,Alfabet).setName("constant")
-	Number = Word(nums)
+	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
+	CryptMsg = Group(CryptOp + lbr + Message + com + Message + rbr).setName("crypt")
-	SMsg = Literal("s") + lbr + Message + rbr
+	SMsg = Group(Literal("s") + lbr + Message + rbr)
 	Message << Or ([TypeMsg, CryptMsg, SMsg, Basic]) + Optional(Literal("'")) 
 
 	# Fact section
-
+	Request = Group("request" + btup(4))
-	Request = "request" + btup(4)
+	Witness = Group("witness" + btup(4))
-	Witness = "witness" + btup(4)
+	Give = Group("give" + lbr + Message + com + ftup(Literal("f"),
-	Give = "give" + lbr + Message + com + ftup(Literal("f"), 1) + rbr
+		1) + rbr)
-	Secret = "secret" + lbr + Message + com + ftup(Literal("f"),1) + rbr
+	Secret = Group("secret" + lbr + Message + com +
-	TimeFact = ftup (Literal("h"), 1)
+			ftup(Literal("f"),1) + rbr)
-	IntruderKnowledge = ftup (Literal("i"), 1)
+	TimeFact = Group(ftup (Literal("h"), 1))
-	MessageFact = ftup(Literal("m"),6)
+	IntruderKnowledge = Group(ftup (Literal("i"), 1))
-	Principal = ftup(Literal("w"), 7)
+	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
+	label = hash + "lb" + equ + rulename + com + "type" + equ + rulecategory
-	rule = State + Optional("\n" + "=>" + "\n" + State)
+	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