diff --git a/scripts/if2spdl/If.py b/scripts/if2spdl/If.py new file mode 100644 index 0000000..ecff5f5 --- /dev/null +++ b/scripts/if2spdl/If.py @@ -0,0 +1,137 @@ +#!/usr/bin/python +# +# If.py +# +# Objects and stuff for the intermediate format +# +firstone = True + +class Atomic(list): + def __init__ (self,l,type=""): + list.__init__(self,l) + self.type = type + + def getType(self): + return self.type + + def __str__(self): + return "".join(self) + + def __repr__(self): + return "Constant<" + str(self) + ">" + +class Special(Atomic): + def __init__ (self,x): + Atomic.__init__(self,[x],"special") + +class Message(list): + def __str__(self): + #return "".join(self) + res = "" + for s in self: + if res != "": + res += "," + res += str(s) + return res + + def subType(self): + return "(generic)" + + def __repr__(self): + return "Message" + self.subType() + "<" + str(self) + ">" + +class MsgList(list): + def __repr__(self): + return "Msglist<" + list.__repr__(self) + ">" + +class Fact(list): + def __repr__(self): + return "Fact<" + list.__repr__(self) + ">" + +class State(list): + def __repr__(self): + return "State<" + list.__repr__(self) + ">" + +class Label(object): + def __init__(self, name, category): + self.name = name + self.category = category + + def __str__(self): + return "lb=" + self.name + ",type=" + self.category + + def __repr__(self): + return str(self) + +class Rule(object): + def __init__(self,left=None,right=None): + self.left = left + self.right = right + self.label = None + + def setLabel(self,label): + self.label = label + + def __str__(self): + res = "Rule:" + if self.label != None: + res += " (" + str(self.label) +")" + res += "\n" + res += str(self.left) + "\n" + res += "=>\n" + res += str(self.right) + "\n" + return res + + def __repr__(self): + return str(self) + +class InitialRule(Rule): + def __str__(self): + return "Initial " + Rule.__str__(self) + +class MessageRule(Rule): + def __init__(self,l,r): + global firstone + + Rule.__init__(self,l,r) + if firstone: + print str(self) + firstone = False + + + def __str__(self): + return "Message " + Rule.__str__(self) + +class GoalRule(Rule): + def __str__(self): + return "Goal " + Rule.__str__(self) + +class CorrespondenceRule(GoalRule): + def __init__(self, l): + GoalRule.__init__(self,l,None) + + def __str__(self): + return "Correspondence " + GoalRule.__str__(self) + +class SecrecyRule(GoalRule): + def __init__(self, l): + GoalRule.__init__(self,l,None) + + def __str__(self): + return "Secrecy " + GoalRule.__str__(self) + +class STSecrecyRule(GoalRule): + def __init__(self, l): + GoalRule.__init__(self,l,None) + + def __str__(self): + return "Short-term Secrecy " + GoalRule.__str__(self) + +class AuthenticateRule(GoalRule): + def __init__(self, l): + GoalRule.__init__(self,l,None) + + def __str__(self): + return "Authenticate " + GoalRule.__str__(self) + + diff --git a/scripts/if2spdl/Ifparser.py b/scripts/if2spdl/Ifparser.py new file mode 100755 index 0000000..e261419 --- /dev/null +++ b/scripts/if2spdl/Ifparser.py @@ -0,0 +1,273 @@ +#!/usr/bin/python + +# requires python-pyparsing module +# http://pyparsing.sourceforge.net/ + +from pyparsing import Literal, alphas, nums, Word, oneOf, Or, Group, \ + restOfLine, Forward, Optional, delimitedList, alphanums,\ + OneOrMore +import If + +typedversion = False + +# Markers: +# +# TODO stuff that still needs to be done. +# DEVIANT stuff that deviates from the original BNF specs in the +# paper. +# TEST test things, remove later + +# Generate parser +# +# Takes a list of tokens, returns +def ruleParser (): + global typedversion + + # ------------------------------------------------------ + # Atomic + # ------------------------------------------------------ + + # Tokens + lbr = Literal("(").suppress() + rbr = Literal(")").suppress() + comma = Literal(",").suppress() + hash = Literal("#") + equ = Literal("=") + implies = Literal("=>").suppress() + dot = Literal(".").suppress() + eol = Literal("\n").suppress() + + # Basic constructors + Alfabet= alphas+nums+"_$" + Number = Word(nums) + + # Typeinfo/Constant + TypeInfo = oneOf ("mr nonce pk sk fu table") + Constant = Word(alphas,Alfabet) + + # Time + nTime = Number + xTime = Literal("xTime") + sTime = Literal("s") + lbr + Group(Number) + rbr + Time = Or([nTime,xTime,sTime]) + + # Const + Const = Forward() + ConstC = Literal("c") + lbr + Constant + comma + Time + rbr + ConstF = Literal("c(ni,ni)") + Const << Or ([ Constant, ConstC, ConstF ]) + + + # Two versions + Variable = Word("x",Alfabet) + if typedversion: + Variable = TypeInfo + lbr + Variable + rbr + + # Optional prime + optprime = Optional(Literal("'")) + + # Atomic + ## DEVIANT : below there is an optprime after the atom. This + ## is not in the BNF. + Atomic = Or([ TypeInfo + lbr + Const + rbr, Variable]) + optprime + Atomic.setParseAction(lambda s,l,t: [ If.Atomic(t) ]) + + ### TEST + #print Const.parseString("Cas'") + #print Atomic.parseString("mr(Cas)'") + #print Atomic.parseString("nonce(Koen)") + + # ------------------------------------------------------ + # Messages + # ------------------------------------------------------ + + # Base forward declaration + Message = Forward() + + + # Agents etc + Agent = Or ([Literal("mr") + lbr + Const + rbr, Variable]) + KeyTable = Or ([Literal("table") + lbr + Const + rbr, Variable]) + KeyTableApp = Literal("tb") + lbr + KeyTable + comma + Agent + rbr + optprime + + # Crypto + pkterm = Literal("pk") + lbr + Const + rbr + optprime + varterm = Variable + optprime + Invertible = Or( [pkterm, KeyTableApp, varterm]) + PublicCypher = Literal("crypt") + lbr + Invertible + comma + Message + rbr + XOR = Literal("rcrypt") + lbr + Message + comma + Message + rbr + SymmetricCypher = Literal("scrypt") + lbr + Message + comma + Message + rbr + futerm = Or([ Literal("fu") + lbr + Const + rbr, Variable ]) + Function = Literal("funct") + lbr + futerm + comma + Message + rbr + + # Message composition + Concatenation = Literal("c") + lbr + Message + comma + Message + rbr + Composed = Or([ Concatenation, SymmetricCypher, XOR, + PublicCypher, Function, KeyTable, KeyTableApp ]) + Message << Or ([Composed, Atomic]) + Message.setParseAction(lambda s,l,t: [ If.Message(t) ]) + + ### TEST + #print Message.parseString("nonce(c(Na,xTime))") + + # ------------------------------------------------------ + # Model of honest agents + # ------------------------------------------------------ + + Boolean = Or ([ Literal("true"), Literal("false"), Variable ]) + Session = Forward() + Session << Or ([ Literal("s") + lbr + Session + rbr, Number, Variable ]) + MsgEtc = Literal("etc") + MsgEtc.setParseAction(lambda s,l,t: [ If.Message([ If.Special("etc") ]) ]) + MsgVariable = Group(Variable) + MsgVariable.setParseAction(lambda s,l,t: [ If.Message([ If.Atomic([ t[0][0] ]) ]) ]) + + MsgList = Forward() + MsgComp = Literal("c") + lbr + Message + comma + MsgList + rbr + MsgComp.setParseAction(lambda s,l,t: [t[1]] + t[2]) + MsgList << Or ([ MsgEtc, MsgVariable, MsgComp ]) + MsgList.setParseAction(lambda s,l,t: [ If.MsgList(t) ]) + + Step = Or ([ Number, Variable ]) + + ### TEST + #print Message.parseString("xKb") + #print MsgList.parseString("etc") + #print MsgList.parseString("c(xKb,etc)") + #print MsgList.parseString("c(xA,c(xB,c(xKa,c(xKa',c(xKb,etc)))))") + + # Principal fact + Principal = Literal("w") + lbr + Step + comma + Agent + comma + Agent + comma + MsgList + comma + MsgList + comma + Boolean + comma + Session + rbr + + # Message fact + MessageFact = Literal("m") + lbr + Step + comma + Agent + comma + Agent + comma + Agent + comma + Message + comma + Session + rbr + + # Goal fact + Secret = Literal("secret") + lbr + Message + Literal("f") + lbr + Session + rbr + rbr + Give = Literal("give") + lbr + Message + Literal("f") + lbr + Session + rbr + rbr + Witness = Literal("witness") + lbr + Agent + comma + Agent + comma + Constant + comma + Message + rbr + Request = Literal("request") + lbr + Agent + comma + Agent + comma + Constant + comma + Message + rbr + GoalFact = Or ([ Secret, Give, Witness, Request ]) + # Goal State + # It actually yields a rule (not a state per se) + Correspondence = Principal + dot + Principal + Correspondence.setParseAction(lambda s,l,t: [ + If.CorrespondenceRule(t) ]) + Secrecy = Literal("secret") + lbr + Literal("xsecret") + comma + Literal("f") + lbr + Session + rbr + rbr + dot + Literal("i") + lbr + Literal("xsecret") + rbr + Secrecy.setParseAction(lambda s,l,t: [ If.SecrecyRule(t) ]) + STSecrecy = Literal("give(xsecret,f(xc)).secret(xsecret,f(xc))") + implies + Literal("i(xsecret)") + STSecrecy.setParseAction(lambda s,l,t: [ + If.STSecrecyRule(t) ]) + Authenticate = Literal("request") + lbr + Agent + comma + Agent + comma + Constant + comma + Message + rbr + Authenticate.setParseAction(lambda s,l,t: [ If.AuthenticateRule(t) ]) + GoalState = Or ([ Correspondence, Secrecy, STSecrecy, Authenticate ]) + + # TimeFact + TimeFact = Literal("h") + lbr + Message + rbr + + # Intruder knowledge + IntruderKnowledge = Literal("i") + lbr + Message + rbr + + # Facts and states + Fact = Or ([ Principal, MessageFact, IntruderKnowledge, TimeFact, Secret, Give, Witness, Request ]) + Fact.setParseAction(lambda s,l,t: [ If.Fact(t) ]) + State = Group(delimitedList (Fact, ".")) ## From initial part of document, not in detailed BNF + State.setParseAction(lambda s,l,t: [ If.State(t) ]) + + # Rules + MFPrincipal = Or ([ MessageFact + dot + Principal, Principal ]) + mr1 = Literal("h") + lbr + Literal("s") + lbr + Literal("xTime") + rbr + rbr + dot + MFPrincipal + mr2 = implies + mr3 = Literal("h") + lbr + Literal("xTime") + rbr + dot + MFPrincipal + Optional(dot + delimitedList(GoalFact, ".")) + MessageRule = Group(mr1) + mr2 + Group(mr3) ## DEVIANT : BNF requires newlines + MessageRule.setParseAction(lambda s,l,t: [ If.MessageRule(t[0],t[1]) ]) + InitialState = Literal("h") + lbr + Literal("xTime") + rbr + dot + State ## DEVIANT : BNF requires newlines + InitialState.setParseAction(lambda s,l,t: [ If.InitialRule(t[2]) ]) + + # Intruder + IntruderRule = Literal("nogniet") + + # Simplification + f_simplif = Literal("f") + lbr + Literal("s") + lbr + Literal ("xc") + rbr + rbr + implies + Literal("f") + lbr + Literal("xc") + rbr ## DEVIANT : EOL removed + matching_request = Witness + dot + Request + implies + no_auth_intruder = Request + implies + SimplificationRule = Or ([ f_simplif, matching_request, no_auth_intruder ]) + + # Compose all rules + Rule = Or([ InitialState, MessageRule, IntruderRule, GoalState, SimplificationRule ]) + + return Rule + +# IFParser +# Does not work for the first line (typed/untyped) +# Depends on ruleParser +def ifParser(): + + comma = Literal(",") + hash = Literal("#") + equal = Literal("=") + + # Rules and labels + 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 + label.setParseAction(lambda s,l,t: [ If.Label(t[3],t[7]) ]) + labeledrule = label + ruleParser() + + def labeledruleAction(s,l,t): + rule = t[1] + if type(rule) == "Rule": + rule.setLabel(t[0]) + return [rule] + + labeledrule.setParseAction(labeledruleAction) + + # A complete file + parser = OneOrMore(labeledrule) + parser.ignore("##" + restOfLine) + + return parser + +# Determine (un)typedness from this line +def typeSwitch(line): + try: + global typedversion + + typeflag = Literal("#") + "option" + Literal("=") + oneOf ("untyped","typed") + res = typeflag.parseString(line) + if res[3] == "untyped": + typedversion = False + elif res[3] == "typed": + typeversion = True + else: + print "Cannot determine whether typed or untyped." + raise ParseException + + 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): + + typeSwitch(lines[0]) + + parser = ifParser() + result = parser.parseString("".join( lines[1:])) + #print result + +# Main code +def main(): + file = open("NSPK_LOWE.if", "r") + linesParse(file.readlines()) + file.close() + + +if __name__ == '__main__': + main() + diff --git a/scripts/if2spdl/Session.vim b/scripts/if2spdl/Session.vim index ffb7fd2..51c0cb9 100644 --- a/scripts/if2spdl/Session.vim +++ b/scripts/if2spdl/Session.vim @@ -30,7 +30,7 @@ set incsearch set nojoinspaces set laststatus=2 set listchars=tab:>.,trail:$ -set makeprg=./parser.py +set makeprg=./Ifparser.py set printencoding=ascii set ruler set scrolloff=2 @@ -50,15 +50,24 @@ if expand('%') == '' && !&modified && line('$') <= 1 && getline(1) == '' let s:wipebuf = bufnr('%') endif set shortmess=aoO -badd +10 if2spdl.py -badd +0 parser.py -args if2spdl.py -edit parser.py +badd +7 If.py +badd +2 Term.py +badd +11 if2spdl.py +badd +11 parser.py +badd +0 Ifparser.py +args If.py +edit Ifparser.py set splitbelow splitright +wincmd _ | wincmd | +vsplit +1wincmd h +wincmd w set nosplitbelow set nosplitright wincmd t set winheight=1 winwidth=1 +exe 'vert 1resize ' . ((&columns * 79 + 79) / 158) +exe 'vert 2resize ' . ((&columns * 78 + 79) / 158) argglobal setlocal noarabic setlocal autoindent @@ -150,16 +159,119 @@ setlocal nowinfixheight setlocal wrap setlocal wrapmargin=0 silent! normal! zE -let s:l = 246 - ((33 * winheight(0) + 27) / 55) +let s:l = 207 - ((32 * winheight(0) + 27) / 55) if s:l < 1 | let s:l = 1 | endif exe s:l normal! zt -246 -normal! 01l +207 +normal! 0 +wincmd w +argglobal +edit If.py +setlocal noarabic +setlocal autoindent +setlocal autoread +setlocal nobinary +setlocal bufhidden= +setlocal buflisted +setlocal buftype= +setlocal nocindent +setlocal cinkeys=0{,0},0),:,0#,!^F,o,O,e +setlocal cinoptions= +setlocal cinwords=if,else,while,do,for,switch +setlocal comments=s1:/*,mb:*,ex:*/,://,b:#,:%,:XCOMM,n:>,fb:- +setlocal commentstring=/*%s*/ +setlocal complete=.,w,b,u,t,i +setlocal completefunc= +setlocal nocopyindent +setlocal define= +setlocal dictionary= +setlocal nodiff +setlocal equalprg= +setlocal errorformat= +setlocal noexpandtab +if &filetype != 'python' +setlocal filetype=python +endif +setlocal foldcolumn=0 +setlocal foldenable +setlocal foldexpr=0 +setlocal foldignore=# +setlocal foldlevel=0 +setlocal foldmarker={{{,}}} +setlocal foldmethod=manual +setlocal foldminlines=1 +setlocal foldnestmax=20 +setlocal foldtext=foldtext() +setlocal formatoptions=cqrt +setlocal formatlistpat=^\\s*\\d\\+[\\]:.)}\\t\ ]\\s* +setlocal grepprg= +setlocal iminsert=2 +setlocal imsearch=2 +setlocal include= +setlocal includeexpr= +setlocal indentexpr=GetPythonIndent(v:lnum) +setlocal indentkeys=0{,0},:,0#,!^F,o,O,e,<:>,=elif,=except +setlocal noinfercase +setlocal iskeyword=@,48-57,_,192-255 +setlocal keymap= +setlocal keywordprg= +setlocal nolinebreak +setlocal nolisp +setlocal nolist +setlocal makeprg= +setlocal matchpairs=(:),{:},[:] +setlocal modeline +setlocal modifiable +setlocal nrformats=octal,hex +setlocal nonumber +setlocal numberwidth=4 +setlocal omnifunc= +setlocal path= +setlocal nopreserveindent +setlocal nopreviewwindow +setlocal quoteescape=\\ +setlocal noreadonly +setlocal norightleft +setlocal rightleftcmd=search +setlocal noscrollbind +setlocal shiftwidth=8 +setlocal noshortname +setlocal nosmartindent +setlocal softtabstop=0 +setlocal nospell +setlocal spellcapcheck=[.?!]\\_[\\])'\"\ \ ]\\+ +setlocal spellfile= +setlocal spelllang=en +setlocal statusline= +setlocal suffixesadd= +setlocal swapfile +setlocal synmaxcol=3000 +if &syntax != 'python' +setlocal syntax=python +endif +setlocal tabstop=8 +setlocal tags= +setlocal textwidth=72 +setlocal thesaurus= +setlocal nowinfixheight +setlocal wrap +setlocal wrapmargin=0 +silent! normal! zE +let s:l = 56 - ((48 * winheight(0) + 27) / 55) +if s:l < 1 | let s:l = 1 | endif +exe s:l +normal! zt +56 +normal! 025l +wincmd w +2wincmd w if exists('s:wipebuf') exe 'bwipe ' . s:wipebuf endif unlet! s:wipebuf +exe 'vert 1resize ' . ((&columns * 79 + 79) / 158) +exe 'vert 2resize ' . ((&columns * 78 + 79) / 158) set winheight=1 winwidth=20 shortmess=at let s:sx = expand(":p:r")."x.vim" if file_readable(s:sx) diff --git a/scripts/if2spdl/parser.py b/scripts/if2spdl/parser.py index 9cff2a7..8181e94 100755 --- a/scripts/if2spdl/parser.py +++ b/scripts/if2spdl/parser.py @@ -7,6 +7,7 @@ from pyparsing import Literal, alphas, nums, Word, oneOf, Or, Group, \ restOfLine, Forward, Optional, delimitedList, alphanums,\ OneOrMore import Term +import If typedversion = False @@ -28,13 +29,13 @@ def ruleParser (): # ------------------------------------------------------ # Tokens - lbr = Literal("(").suppress() - rbr = Literal(")").suppress() - comma = Literal(",").suppress() - hash = Literal("#").suppress() - equ = Literal("=").suppress() - implies = Literal("=>").suppress() - dot = Literal(".").suppress() + lbr = Literal("(") + rbr = Literal(")") + comma = Literal(",") + hash = Literal("#") + equ = Literal("=") + implies = Literal("=>") + dot = Literal(".") eol = Literal("\n").suppress() # Basic constructors @@ -46,25 +47,25 @@ def ruleParser (): TypeInfo = oneOf ("mr nonce pk sk fu table") TypeInfo.setParseAction(lambda s,l,t: [ "typeinfo", Term.TermConstant(t[0]) ]) Constant = Word(alphas,Alfabet) - Constant.setParseAction(lambda s,l,t: [ "constant", Term.TermConstant(t[0]) ]) + Constant.setParseAction(lambda s,l,t: [ Term.TermConstant(t[0]) ]) # Time - nTime = Group(Number) - nTime.setParseAction(lambda s,l,t: ["n", t[0] ]) + nTime = Number xTime = Literal("xTime") - xTime.setParseAction(lambda s,l,t: ["x", t[0] ]) sTime = Literal("s").suppress() + lbr + Group(Number) + rbr - sTime.setParseAction(lambda s,l,t: ["s", t[0] ]) Time = Or([nTime,xTime,sTime]) - Time.setParseAction(lambda s,l,t: ["time", t[0],t[1] ]) # Const Const = Forward() - Const << Or ([ Constant, Literal("c") + lbr + Constant + comma + Time + rbr, Literal("c(ni,ni)") ]) + ConstC = Literal("c") + lbr + Constant + comma + Time + rbr + ConstF = Literal("c(ni,ni)") + Const << Or ([ Constant, ConstC, ConstF ]) + + Const.setParseAction(lambda s,l,t: [ If.Constant("".join(t)) ]) # Two versions Variable = Word("x",Alfabet) - Variable.setParseAction(lambda s,l,t: [ "v", Term.TermVariable(t[0],None) ]) + Variable.setParseAction(lambda s,l,t: [ Term.TermVariable(t[0]+"V",None) ]) if typedversion: Variable = TypeInfo + lbr + Variable + rbr @@ -99,6 +100,7 @@ def ruleParser (): varterm = Variable + optprime Invertible = Or( [pkterm, KeyTableApp, varterm]) PublicCypher = Literal("crypt") + lbr + Invertible + comma + Message + rbr + PublicCypher.setParseAction(lambda s,l,t: [ Term.TermEncrypt(t[2],t[1]) ]) XOR = Literal("rcrypt") + lbr + Message + comma + Message + rbr SymmetricCypher = Literal("scrypt") + lbr + Message + comma + Message + rbr futerm = Or([ Literal("fu") + lbr + Const + rbr, Variable ]) @@ -106,6 +108,7 @@ def ruleParser (): # Message composition Concatenation = Literal("c") + lbr + Message + comma + Message + rbr + Concatenation.setParseAction(lambda s,l,t: [ Term.TermTuple(t[1],t[2]) ]) Composed = Or([ Concatenation, SymmetricCypher, XOR, PublicCypher, Function, KeyTable, KeyTableApp ]) Message << Or ([Composed, Atomic]) @@ -136,6 +139,7 @@ def ruleParser (): # Principal fact Principal = Literal("w") + lbr + Step + comma + Agent + comma + Agent + comma + MsgList + comma + MsgList + comma + Boolean + comma + Session + rbr + Principal.setParseAction(lambda s,l,t: [ "Principal", t]) # Message fact MessageFact = Literal("m") + lbr + Step + comma + Agent + comma + Agent + comma + Agent + comma + Message + comma + Session + rbr @@ -167,7 +171,7 @@ def ruleParser (): mr1 = Literal("h") + lbr + Literal("s") + lbr + Literal("xTime") + rbr + rbr + dot + MFPrincipal mr2 = implies mr3 = Literal("h") + lbr + Literal("xTime") + rbr + dot + MFPrincipal + Optional(dot + delimitedList(GoalFact, ".")) - MessageRule = mr1 + mr2 + mr3 ## DEVIANT : BNF requires newlines + MessageRule = Group(mr1) + mr2 + Group(mr3) ## DEVIANT : BNF requires newlines InitialState = Literal("h") + lbr + Literal("xTime") + rbr + dot + State ## DEVIANT : BNF requires newlines # Intruder @@ -200,13 +204,14 @@ def ifParser(): labeledrule = Group(label) + Group(ruleParser()) def labeledruleAction(s,l,t): - print "-----------------" - print "- Detected rule -" - print "-----------------" + if t[0][3] == "Protocol_Rules": + print "-----------------" + print "- Detected rule -" + print "-----------------" - print t[0] - print t[1] - print + print t[0] + print t[1] + print labeledrule.setParseAction(labeledruleAction)