scyther/scripts/if2spdl/Ifparser.py

313 lines
10 KiB
Python
Raw Normal View History

2005-12-03 16:12:58 +00:00
#!/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
lbrX = Literal("(")
rbrX = Literal(")")
commaX = Literal(",")
2005-12-03 16:12:58 +00:00
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") + lbrX + Number + rbrX
2005-12-03 16:12:58 +00:00
Time = Or([nTime,xTime,sTime])
# Const
Const = Forward()
ConstC = Literal("c") + lbrX + Constant + commaX + Time + rbrX
2005-12-03 16:12:58 +00:00
ConstF = Literal("c(ni,ni)")
Const << Or ([ Constant, ConstC, ConstF ])
def stringize(s,l,t):
return [ "".join(t) ]
Const.setParseAction(stringize)
# Optional prime
def optprimeaction(s,l,t):
if len(t) == 0:
return [ "" ]
else:
return t
optprime = Optional(Literal("'"))
optprime.setParseAction(optprimeaction)
2005-12-03 16:12:58 +00:00
# Two versions
if typedversion:
Variable = Word("x",Alfabet)
Variable = TypeInfo + lbr + Variable + rbr + optprime
Variable.setParseAction(lambda s,l,t: [
If.Variable(t[0],t[1],t[2]) ])
else:
Variable = Word("x",Alfabet) + optprime
Variable.setParseAction(lambda s,l,t: [
If.Variable("untyped",t[0],t[1]) ])
2005-12-03 16:12:58 +00:00
# Atomic
## DEVIANT : below there is an optprime after the atom. This
## is not in the BNF.
TypedConstant = TypeInfo + lbr + Const + rbr + optprime
TypedConstant.setParseAction(lambda s,l,t: [
If.Constant(t[0],t[1],t[2]) ])
Atomic = Or(TypedConstant, Variable)
2005-12-03 16:12:58 +00:00
### TEST
print Atomic.parseString("mr(Cas)'")
print Atomic.parseString("nonce(Koen)")
2005-12-03 16:12:58 +00:00
# ------------------------------------------------------
# Messages
# ------------------------------------------------------
# Base forward declaration
Message = Forward()
# Agents etc
AgentMr = Literal("mr") + lbr + Const + rbr
AgentMr.setParseAction(lambda s,l,t: [ If.Constant(t[0],t[1]) ])
Agent = Or ([AgentMr, Variable])
# TODO Not implemented yet
2005-12-03 16:12:58 +00:00
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
pkterm.setParseAction(lambda s,l,t: [ If.PublicKey(t[0],t[1],t[2]) ])
##varterm = Variable + optprime ### Variable already has an optprime
varterm = Variable
2005-12-03 16:12:58 +00:00
Invertible = Or( [pkterm, KeyTableApp, varterm])
PublicCypher = Literal("crypt") + lbr + Invertible + comma + Message + rbr
PublicCypher.setParseAction(lambda s,l,t: [ If.PublicCrypt(t[1],t[2]) ])
2005-12-03 16:12:58 +00:00
XOR = Literal("rcrypt") + lbr + Message + comma + Message + rbr
XOR.setParseAction(lambda s,l,t: [ If.XOR(t[1],t[2]) ])
2005-12-03 16:12:58 +00:00
SymmetricCypher = Literal("scrypt") + lbr + Message + comma + Message + rbr
SymmetricCypher.setParseAction(lambda s,l,t: [ If.SymmetricCrypt(t[1],t[2]) ])
# TODO Not implemented yet
2005-12-03 16:12:58 +00:00
futerm = Or([ Literal("fu") + lbr + Const + rbr, Variable ])
Function = Literal("funct") + lbr + futerm + comma + Message + rbr
Concatenation = Literal("c").suppress() + lbr + Message + comma + Message + rbr
Concatenation.setParseAction(lambda s,l,t: [ If.Composed(t[0],t[1]) ])
# Message composition
2005-12-03 16:12:58 +00:00
Composed = Or([ Concatenation, SymmetricCypher, XOR,
PublicCypher, Function, KeyTable, KeyTableApp ])
Message << Or ([Composed, Atomic])
### 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.MsgList([If.Constant("special","etc") ]) ])
MsgVar = Group(Variable)
MsgVar.setParseAction(lambda s,l,t: [ If.MsgList(t) ])
2005-12-03 16:12:58 +00:00
MsgList = Forward()
MsgComp = Literal("c") + lbr + Message + comma + MsgList + rbr
MsgComp.setParseAction(lambda s,l,t: [ If.MsgList([ t[1] ]) + t[2] ])
MsgList << Or ([ MsgEtc, Variable, MsgComp ])
2005-12-03 16:12:58 +00:00
Step = Or ([ Number, Variable ])
### TEST
#print Message.parseString("xKb")
#print Message.parseString("mr(Cas)")
2005-12-03 16:12:58 +00:00
#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
2005-12-03 16:48:10 +00:00
Principal.setParseAction(lambda s,l,t: [ If.PrincipalFact(t[1:]) ])
2005-12-03 16:12:58 +00:00
# Message fact
MessageFact = Literal("m") + lbr + Step + comma + Agent + comma + Agent + comma + Agent + comma + Message + comma + Session + rbr
2005-12-03 16:48:10 +00:00
MessageFact.setParseAction(lambda s,l,t: [ If.MessageFact(t[1:]) ])
2005-12-03 16:12:58 +00:00
# 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 ])
2005-12-03 16:48:10 +00:00
GoalFact.setParseAction(lambda s,l,t: [ If.GoalFact(t) ])
2005-12-03 16:12:58 +00:00
# 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
2005-12-03 16:48:10 +00:00
TimeFact.setParseAction(lambda s,l,t: [ If.TimeFact(t[1]) ])
2005-12-03 16:12:58 +00:00
# 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
2005-12-03 16:48:10 +00:00
MessageRule.setParseAction(lambda s,l,t: [
If.MessageRule(t[0][3],t[1][2:]) ])
2005-12-03 16:12:58 +00:00
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]
2005-12-03 16:48:10 +00:00
rule.setLabel(t[0])
2005-12-03 16:12:58 +00:00
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:]))
2005-12-03 16:48:10 +00:00
### TEST
2005-12-03 16:12:58 +00:00
#print result
# Main code
def main():
file = open("NSPK_LOWE.if", "r")
linesParse(file.readlines())
file.close()
if __name__ == '__main__':
main()