From dbc5d62ef6395d2272b38a1a8b37ef252407ddf5 Mon Sep 17 00:00:00 2001 From: ccremers Date: Tue, 29 Nov 2005 14:16:36 +0000 Subject: [PATCH] - Much improved parser. --- scripts/if2spdl/Session.vim | 128 ++----------------- scripts/if2spdl/notes.txt | 14 +++ scripts/if2spdl/parser.py | 238 ++++++++++++++++-------------------- 3 files changed, 131 insertions(+), 249 deletions(-) create mode 100644 scripts/if2spdl/notes.txt diff --git a/scripts/if2spdl/Session.vim b/scripts/if2spdl/Session.vim index b86d4e4..ffb7fd2 100644 --- a/scripts/if2spdl/Session.vim +++ b/scripts/if2spdl/Session.vim @@ -4,7 +4,6 @@ set cpo&vim imap :call Cream_replacemulti() map! nnoremap  :exe 'silent! normal! za'.(foldlevel('.')?'':'l') -map "," :!./parser.py map , :make nmap :call Cream_replacemulti() vmap :call Cream_replacemulti() @@ -31,7 +30,7 @@ set incsearch set nojoinspaces set laststatus=2 set listchars=tab:>.,trail:$ -set makeprg=./if2spdl.py +set makeprg=./parser.py set printencoding=ascii set ruler set scrolloff=2 @@ -43,7 +42,6 @@ set viminfo=%,'50,\"1000,:100,f1,n~/.viminfo set visualbell set whichwrap=<,>,h,l set wildmenu -set window=30 let s:so_save = &so | let s:siso_save = &siso | set so=0 siso=0 let v:this_session=expand(":p") silent only @@ -52,25 +50,17 @@ if expand('%') == '' && !&modified && line('$') <= 1 && getline(1) == '' let s:wipebuf = bufnr('%') endif set shortmess=aoO -badd +9 parser.py -badd +0 NSPK_LOWE.if1 -badd +8 NSPK_LOWE.if -badd +6 if2spdl.py -badd +0 generator.py -args parser.py -edit generator.py +badd +10 if2spdl.py +badd +0 parser.py +args if2spdl.py +edit parser.py set splitbelow splitright -wincmd _ | wincmd | -split -1wincmd k -wincmd w set nosplitbelow set nosplitright wincmd t set winheight=1 winwidth=1 -exe '1resize ' . ((&lines * 15 + 15) / 31) -exe '2resize ' . ((&lines * 13 + 15) / 31) argglobal +setlocal noarabic setlocal autoindent setlocal autoread setlocal nobinary @@ -116,6 +106,7 @@ 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 @@ -133,6 +124,8 @@ setlocal nopreserveindent setlocal nopreviewwindow setlocal quoteescape=\\ setlocal noreadonly +setlocal norightleft +setlocal rightleftcmd=search setlocal noscrollbind setlocal shiftwidth=8 setlocal noshortname @@ -157,115 +150,16 @@ setlocal nowinfixheight setlocal wrap setlocal wrapmargin=0 silent! normal! zE -let s:l = 4 - ((3 * winheight(0) + 7) / 15) +let s:l = 246 - ((33 * winheight(0) + 27) / 55) if s:l < 1 | let s:l = 1 | endif exe s:l normal! zt -4 +246 normal! 01l -wincmd w -argglobal -edit if2spdl.py -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 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 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 = 13 - ((9 * winheight(0) + 6) / 13) -if s:l < 1 | let s:l = 1 | endif -exe s:l -normal! zt -13 -normal! 0 -wincmd w -2wincmd w if exists('s:wipebuf') exe 'bwipe ' . s:wipebuf endif unlet! s:wipebuf -exe '1resize ' . ((&lines * 15 + 15) / 31) -exe '2resize ' . ((&lines * 13 + 15) / 31) 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/notes.txt b/scripts/if2spdl/notes.txt new file mode 100644 index 0000000..aad128c --- /dev/null +++ b/scripts/if2spdl/notes.txt @@ -0,0 +1,14 @@ +Notes +----- + +Regarding the AVISPA IF report: + +- Messages do not seem to contain Varable' as an option, seems to be + flaw in the BNF. +- State has no BNF definition in the second half, it seems. +- Is Fact well-defined? +- Authenticate has no parameters in it (only constants) + STSecrecy + matching_request + + diff --git a/scripts/if2spdl/parser.py b/scripts/if2spdl/parser.py index 1c84ea9..3f7865b 100755 --- a/scripts/if2spdl/parser.py +++ b/scripts/if2spdl/parser.py @@ -4,15 +4,23 @@ # http://pyparsing.sourceforge.net/ from pyparsing import Literal, alphas, nums, Word, oneOf, Or, Group, \ - restOfLine, Forward, Optional, delimitedList + restOfLine, Forward, Optional, delimitedList, alphanums,\ + OneOrMore import Term typedversion = False -# Generate atom parser +# 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 atomsParser (): +def ruleParser (): global typedversion # ------------------------------------------------------ @@ -37,30 +45,41 @@ def atomsParser (): # Typeinfo/Constant TypeInfo = oneOf ("mr nonce pk sk fu table") TypeInfo.setParseAction(lambda s,l,t: [ "typeinfo", Term.TermConstant(t[0]) ]) - Const = Word(alphas,Alfabet) - Const.setParseAction(lambda s,l,t: [ "constant", Term.TermConstant(t[0]) ]) + Constant = Word(alphas,Alfabet) + Constant.setParseAction(lambda s,l,t: [ "constant", Term.TermConstant(t[0]) ]) # Time nTime = Group(Number) nTime.setParseAction(lambda s,l,t: ["n", t[0] ]) xTime = Literal("xTime") - xTime.setParseAction(lambda s,l,t: ["x", 0 ]) + 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)") ]) + # Two versions Variable = Word("x",Alfabet) Variable.setParseAction(lambda s,l,t: [ "v", Term.TermVariable(t[0],None) ]) if typedversion: - Variable = TypeInfo + "(" + Variable + ")" + Variable = TypeInfo + lbr + Variable + rbr + + # Optional prime + optprime = Optional(Literal("'")) # Atomic - Atomic = Or([ TypeInfo + lbr + Const + rbr, Variable]) + ## DEVIANT : below there is an optprime after the atom. This + ## is not in the BNF. + Atomic = Or([ TypeInfo + lbr + Const + rbr, Variable]) + optprime ### TEST - print Time.parseString("s(25)") + #print Time.parseString("s(25)") + #print Variable.parseString("xCas") + #print Atomic.parseString("nonce(Koen)") # ------------------------------------------------------ # Messages @@ -69,8 +88,6 @@ def atomsParser (): # Base forward declaration Message = Forward() - # Optional prime - optprime = Optional(Literal("'")) # Agents etc Agent = Or ([Literal("mr") + lbr + Const + rbr, Variable]) @@ -91,7 +108,10 @@ def atomsParser (): Concatenation = Literal("c") + lbr + Message + comma + Message + rbr Composed = Or([ Concatenation, SymmetricCypher, XOR, PublicCypher, Function, KeyTable, KeyTableApp ]) - Message = Or ([Composed, Atomic]) + Message << Or ([Composed, Atomic]) + + ### TEST + #print Message.parseString("nonce(c(Na,xTime))") # ------------------------------------------------------ # Model of honest agents @@ -99,18 +119,20 @@ def atomsParser (): Boolean = Or ([ Literal("true"), Literal("false"), Variable ]) Session = Forward() - Session = Or ([ Literal("s") + lbr + Session + rbr, Number, Variable ]) - MsgList = Forward() + Session << Or ([ Literal("s") + lbr + Session + rbr, Number, Variable ]) MsgEtc = Literal("etc") + + MsgList = Forward() MsgComp = Literal("c") + lbr + Message + comma + MsgList + rbr - MsgList = Or ([ MsgEtc, Variable, MsgComp ]) + MsgList << Or ([ MsgEtc, Variable, MsgComp ]) + Step = Or ([ Number, Variable ]) ### TEST - print Message.parseString("xKb") - print MsgList.parseString("etc") - print MsgComp.parseString("c(xKb,etc)") - print MsgList.parseString("c(xA,c(xB,c(xKa,c(xKa',c(xKb,etc)))))") + #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 @@ -119,148 +141,100 @@ def atomsParser (): MessageFact = Literal("m") + lbr + Step + comma + Agent + comma + Agent + comma + Agent + comma + Message + comma + Session + rbr # Goal fact - GoalFact = Literal ("nogniet") - GoalState = Literal ("nogniet") + Correspondence = Principal + dot + Principal + Secret = Literal("secret") + lbr + Message + Literal("f") + lbr + Session + rbr + rbr + Secrecy = Literal("secret") + lbr + Literal("xsecret") + comma + Literal("f") + lbr + Session + rbr + rbr + dot + Literal("i") + lbr + Literal("xsecret") + rbr + Give = Literal("give") + lbr + Message + Literal("f") + lbr + Session + rbr + rbr + STSecrecy = Literal("give(xsecret,f(xc)).secret(xsecret,f(xc))") + implies + Literal("i(xsecret)") + Witness = Literal("witness") + lbr + Agent + comma + Agent + comma + Constant + comma + Message + rbr + Request = Literal("request") + lbr + Agent + comma + Agent + comma + Constant + comma + Message + rbr + Authenticate = Literal("request") + lbr + Agent + comma + Agent + comma + Constant + comma + Message + rbr + GoalFact = Or ([ Correspondence, Secrecy, STSecrecy, Authenticate ]) + GoalState = Or ([ Secret, Give, Witness, Request ]) # Facts and states - Fact = Or ([ Principal, MessageFact ]) - State = Group(delimitedList (Fact, ".")) + Fact = Or ([ Principal, MessageFact, GoalFact ]) ## Not well defined in BNF + State = Group(delimitedList (Fact, ".")) ## From initial part of document, not in detailed BNF # Rules - mr1 = Literal("h") + lbr + Literal("s") + lbr + Literal("xTime") + rbr + rbr + dot + State + 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 + MessageFact + dot + Principal + dot + GoalFact + eol - MessageRule = mr1 + eol + mr2 + eol + mr3 + eol - InitialState = Literal("h") + lbr + Literal("xTime") + rbr + dot + State + eol + mr3 = Literal("h") + lbr + Literal("xTime") + rbr + dot + MFPrincipal + Optional(dot + delimitedList(GoalFact, ".")) + MessageRule = mr1 + mr2 + mr3 ## DEVIANT : BNF requires newlines + InitialState = Literal("h") + lbr + Literal("xTime") + rbr + dot + State ## DEVIANT : BNF requires newlines # Intruder IntruderRule = Literal("nogniet") # Simplification - SimplificationRule = Literal("nogniet") + 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 - print Rule.parseFile("test.if") +# IFParser +# Does not work for the first line (typed/untyped) +# Depends on ruleParser +def ifParser(): - - - - -def ifParse (str): - # Tokens - lbr = Literal("(").suppress() - rbr = Literal(")").suppress() comma = Literal(",").suppress() hash = Literal("#").suppress() - equ = Literal("=").suppress() - implies = Literal("=>").suppress() - - # Functions to construct tuples etc - def bracket(x): - return lbr + x + rbr - - def ntup(n): - x = Message - while n > 1: - x = x + comma + 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).setParseAction(lambda s,l,t: [ Term.TermVariable(t[0],None) ]) - Constant = Word(alphas,Alfabet).setParseAction(lambda s,l,t: [ Term.TermConstant(t[0]) ]) - Number = Word(nums).setParseAction(lambda s,l,t: [ Term.TermConstant(t[0]) ]) - - Basic = MatchFirst([ Variable, Constant, Number ]) - - # Message definition is recursive - Message = Forward() - - def parseType(s,l,t): - if t[0][0] == "pk": - # Public key thing, that's not really a type for - # us but a function - return [Term.TermEncrypt(t[0][1], t[0][0]) ] - - 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(parseType) - - def parseCrypt(s,l,t): - # Crypto types are ignored for now - type = t[0][0] - if type == "c": - return [Term.TermTuple( t[0][1],t[0][2] ) ] - return [Term.TermEncrypt(t[0][2],t[0][1])] - - CryptOp = oneOf ("crypt scrypt c funct rcrypt tb") - CryptMsg = Group(CryptOp + lbr + Message + comma + 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) - - 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)) - Witness = Group("witness" + btup(4)) - Give = Group("give" + lbr + Message + comma + ftup(Literal("f"), - 1) + rbr) - Secret = Group("secret" + lbr + Message + comma + - 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 - - #State = Fact + OptioZeroOrMore ("." + Fact) - State = Group(delimitedList (Fact, ".")) + equal = Literal("=").suppress() # Rules and labels rulename = Word (alphanums + "_") rulecategory = oneOf("Protocol_Rules Invariant_Rules Decomposition_Rules Intruder_Rules Init Goal") - label = hash + "lb" + equ + rulename + comma + "type" + equ + rulecategory - rule = Group(State + Optional(implies + State)) - labeledrule = Group(label + rule) - typeflag = hash + "option" + equ + oneOf ("untyped","typed") + label = hash + Literal("lb") + equal + rulename + comma + Literal("type") + equal + rulecategory + labeledrule = Group(label + ruleParser()) # A complete file - iffile = typeflag + Group(OneOrMore(labeledrule)) - - parser = iffile + parser = Group(OneOrMore(labeledrule)) parser.ignore("##" + restOfLine) - return parser.parseString(str) + 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 + + +# Parse an entire file, including the first one +def linesParse(lines): + + typeSwitch(lines[0]) + + parser = ifParser() + result = parser.parseString("".join( lines[1:])) + + for x in result: + print x + +# Main code def main(): - global typedversion + file = open("NSPK_LOWE.if", "r") + linesParse(file.readlines()) + file.close() - typedversion = False - atomsParser() if __name__ == '__main__': main()