Skip to content

Commit

Permalink
edit/add files, models, and proofs
Browse files Browse the repository at this point in the history
  • Loading branch information
@jorgetp
jorgetp committed Feb 12, 2021
1 parent 28d26ca commit 5327896
Show file tree
Hide file tree
Showing 75 changed files with 1,051,158 additions and 539 deletions.
326 changes: 153 additions & 173 deletions Contactless.spthy
View file

Large diffs are not rendered by default.

177 changes: 81 additions & 96 deletions Makefile
View file
Original file line number Diff line number Diff line change
@@ -1,70 +1,68 @@
TAMARIN = tamarin-prover
TFLAGS = +RTS -N10 -M20G -RTS
DECOMMENT = tools/decomment
PREFIXDIR = models-n-proofs
SEPARATOR = ==============================================================================

#configuration variables
generic = Contactless
kernel = Mastercard
auth = CDA
brand = Visa
auth = EMV
CVM = OnlinePIN
value = Low
authz = Offline
softfix = No
hardfix = No
paynet = AID

#other variables
decomment = Yes

#to uncomment the code blocks that follow the selected configuration
#uncomment the code blocks that follow the selected configuration
left1 = if(\(|\(([a-zA-Z0-9]+\|)+)
left2 = endif(\(|\(([a-zA-Z0-9]+\|)+)
right = (\)|(\|[a-zA-Z0-9]+)+\))

regex0 = \/\*$(left1)$(kernel)$(right) *| *$(left2)$(kernel)$(right)\*\/
regex1 = \/\*$(left1)$(auth)$(right) *| *$(left2)$(auth)$(right)\*\/
regex2 = \/\*$(left1)$(CVM)$(right) *| *$(left2)$(CVM)$(right)\*\/
regex3 = \/\*$(left1)$(value)$(right) *| *$(left2)$(value)$(right)\*\/
regex4 = \/\*$(left1)$(authz)$(right) *| *$(left2)$(authz)$(right)\*\/
regex5 = \/\*$(left1)Fix$(right) *| *$(left2)Fix$(right)\*\/

#contact
ifeq ($(generic), Contact)
regex = ($(regex1)|$(regex2)|$(regex4))
theory = Contact_$(auth)_$(CVM)_$(authz)
oracle = Contact.oracle
brand_regex = \/\*$(left1)$(brand)$(right) *| *$(left2)$(brand)$(right)\*\/
auth_regex = \/\*$(left1)$(auth)$(right) *| *$(left2)$(auth)$(right)\*\/
CVM_regex = \/\*$(left1)$(CVM)$(right) *| *$(left2)$(CVM)$(right)\*\/
value_regex = \/\*$(left1)$(value)$(right) *| *$(left2)$(value)$(right)\*\/
authz_regex = \/\*$(left1)$(authz)$(right) *| *$(left2)$(authz)$(right)\*\/
soft_fix_regex = \/\*$(left1)SoftFix$(right) *| *$(left2)SoftFix$(right)\*\/
hard_fix_regex = \/\*$(left1)HardFix$(right) *| *$(left2)HardFix$(right)\*\/
paynet_regex = \/\*$(left1)$(paynet)$(right) *| *$(left2)$(paynet)$(right)\*\/

ifndef dir
dir = $(PREFIXDIR)/contact
endif
dir = $(PREFIXDIR)
endif

#contactless
ifeq ($(generic), Contactless)
ifndef dir
dir = $(PREFIXDIR)/contactless
ifeq ($(brand), Mastercard)
CVM_regex_ = |$(CVM_regex)
CVM_ = _$(CVM)
endif
ifeq ($(kernel), Mastercard)
regex = ($(regex0)|$(regex1)|$(regex2)|$(regex3))
theory = Mastercard_$(auth)_$(CVM)_$(value)
oracle = Mastercard.oracle
else

ifdef fix
regex = ($(regex0)|$(regex1)|$(regex3)|$(regex5))
theory = Visa_$(auth)_$(value)_Fix
else
regex = ($(regex0)|$(regex1)|$(regex3))
theory = Visa_$(auth)_$(value)

ifeq ($(paynet), PAN)
paynet_ = _PaynetPAN
endif
oracle = Visa.oracle

regex = ($(brand_regex)|$(auth_regex)$(CVM_regex_)|$(value_regex)|$(paynet_regex))
theory = $(brand)_$(auth)$(CVM_)_$(value)$(paynet_)

ifeq ($(softfix), Yes)
regex = $(soft_fix_regex)
theory = Contactless_SoftFix
endif

ifeq ($(hardfix), Yes)
regex = $(hard_fix_regex)
theory = Contactless_HardFix
endif

#use oracle if indicated
ifdef oracle
ifndef oracle
oracle = $(brand).oracle
endif
ifeq ($(oracle),$(wildcard $(oracle)))
_oracle = --heuristic=O --oraclename=$(oracle)
endif
endif

#prove only one lemma if indicated
ifdef lemma
Expand All @@ -77,7 +75,7 @@ cmd = $(TAMARIN) --prove$(_lemma) $(dir)/$(theory).spthy $(_oracle) $(TFLAGS) --
proof:
#Create directory for specific models and their proofs
mkdir -p $(dir)

#Generate theory file $(theory).spthy
sed -E 's/$(regex)//g' $(generic).spthy > $(dir)/$(theory).tmp
sed -E 's/theory .*/theory $(theory)/' $(dir)/$(theory).tmp > $(dir)/$(theory).spthy
Expand Down Expand Up @@ -111,73 +109,60 @@ endif

#for clarity, will use below some redundant variable assignments
####
contactless:
#mastercard:
mastercard:
#SDA
$(MAKE) kernel=Mastercard auth=SDA CVM=NoPIN value=Low
$(MAKE) kernel=Mastercard auth=SDA CVM=NoPIN value=High
$(MAKE) kernel=Mastercard auth=SDA CVM=OnlinePIN value=Low
$(MAKE) kernel=Mastercard auth=SDA CVM=OnlinePIN value=High
$(MAKE) brand=Mastercard auth=SDA CVM=NoPIN value=Low
$(MAKE) brand=Mastercard auth=SDA CVM=NoPIN value=High
$(MAKE) brand=Mastercard auth=SDA CVM=OnlinePIN value=Low
$(MAKE) brand=Mastercard auth=SDA CVM=OnlinePIN value=High
#DDA
$(MAKE) kernel=Mastercard auth=DDA CVM=NoPIN value=Low
$(MAKE) kernel=Mastercard auth=DDA CVM=NoPIN value=High
$(MAKE) kernel=Mastercard auth=DDA CVM=OnlinePIN value=Low
$(MAKE) kernel=Mastercard auth=DDA CVM=OnlinePIN value=High
$(MAKE) brand=Mastercard auth=DDA CVM=NoPIN value=Low
$(MAKE) brand=Mastercard auth=DDA CVM=NoPIN value=High
$(MAKE) brand=Mastercard auth=DDA CVM=OnlinePIN value=Low
$(MAKE) brand=Mastercard auth=DDA CVM=OnlinePIN value=High
#CDA
$(MAKE) kernel=Mastercard auth=CDA CVM=NoPIN value=Low
$(MAKE) kernel=Mastercard auth=CDA CVM=NoPIN value=High
$(MAKE) kernel=Mastercard auth=CDA CVM=OnlinePIN value=Low
$(MAKE) kernel=Mastercard auth=CDA CVM=OnlinePIN value=High

#visa:
#EMV mode
$(MAKE) kernel=Visa auth=EMV value=Low
$(MAKE) kernel=Visa auth=EMV value=High
#DDA mode
$(MAKE) kernel=Visa auth=DDA value=Low
$(MAKE) kernel=Visa auth=DDA value=High

#visa-fix:
$(MAKE) kernel=Visa auth=DDA value=Low fix=Yes
$(MAKE) brand=Mastercard auth=CDA CVM=NoPIN value=Low
$(MAKE) brand=Mastercard auth=CDA CVM=NoPIN value=High
$(MAKE) brand=Mastercard auth=CDA CVM=OnlinePIN value=Low
$(MAKE) brand=Mastercard auth=CDA CVM=OnlinePIN value=High

contact:
#contact-offline:
#SDA
$(MAKE) generic=Contact auth=SDA CVM=NoPIN authz=Offline
$(MAKE) generic=Contact auth=SDA CVM=PlainPIN authz=Offline
$(MAKE) generic=Contact auth=SDA CVM=EncPIN authz=Offline
$(MAKE) generic=Contact auth=SDA CVM=OnlinePIN authz=Offline
$(MAKE) brand=Mastercard auth=SDA CVM=NoPIN value=Low paynet=PAN
$(MAKE) brand=Mastercard auth=SDA CVM=NoPIN value=High paynet=PAN
$(MAKE) brand=Mastercard auth=SDA CVM=OnlinePIN value=Low paynet=PAN
$(MAKE) brand=Mastercard auth=SDA CVM=OnlinePIN value=High paynet=PAN
#DDA
$(MAKE) generic=Contact auth=DDA CVM=NoPIN authz=Offline
$(MAKE) generic=Contact auth=DDA CVM=PlainPIN authz=Offline
$(MAKE) generic=Contact auth=DDA CVM=EncPIN authz=Offline
$(MAKE) generic=Contact auth=DDA CVM=OnlinePIN authz=Offline
$(MAKE) brand=Mastercard auth=DDA CVM=NoPIN value=Low paynet=PAN
$(MAKE) brand=Mastercard auth=DDA CVM=NoPIN value=High paynet=PAN
$(MAKE) brand=Mastercard auth=DDA CVM=OnlinePIN value=Low paynet=PAN
$(MAKE) brand=Mastercard auth=DDA CVM=OnlinePIN value=High paynet=PAN
#CDA
$(MAKE) generic=Contact auth=CDA CVM=NoPIN authz=Offline
$(MAKE) generic=Contact auth=CDA CVM=PlainPIN authz=Offline
$(MAKE) generic=Contact auth=CDA CVM=EncPIN authz=Offline
$(MAKE) generic=Contact auth=CDA CVM=OnlinePIN authz=Offline
$(MAKE) brand=Mastercard auth=CDA CVM=NoPIN value=Low paynet=PAN
$(MAKE) brand=Mastercard auth=CDA CVM=NoPIN value=High paynet=PAN
$(MAKE) brand=Mastercard auth=CDA CVM=OnlinePIN value=Low paynet=PAN
$(MAKE) brand=Mastercard auth=CDA CVM=OnlinePIN value=High paynet=PAN

#contact-online:
#SDA
$(MAKE) generic=Contact auth=SDA CVM=NoPIN authz=Online
$(MAKE) generic=Contact auth=SDA CVM=PlainPIN authz=Online
$(MAKE) generic=Contact auth=SDA CVM=EncPIN authz=Online
$(MAKE) generic=Contact auth=SDA CVM=OnlinePIN authz=Online
#DDA
$(MAKE) generic=Contact auth=DDA CVM=NoPIN authz=Online
$(MAKE) generic=Contact auth=DDA CVM=PlainPIN authz=Online
$(MAKE) generic=Contact auth=DDA CVM=EncPIN authz=Online
$(MAKE) generic=Contact auth=DDA CVM=OnlinePIN authz=Online
#CDA
$(MAKE) generic=Contact auth=CDA CVM=NoPIN authz=Online
$(MAKE) generic=Contact auth=CDA CVM=PlainPIN authz=Online
$(MAKE) generic=Contact auth=CDA CVM=EncPIN authz=Online
$(MAKE) generic=Contact auth=CDA CVM=OnlinePIN authz=Online
visa:
#EMV mode
$(MAKE) brand=Visa auth=EMV value=Low
$(MAKE) brand=Visa auth=EMV value=High
#DDA mode
$(MAKE) brand=Visa auth=DDA value=Low
$(MAKE) brand=Visa auth=DDA value=High

#EMV mode
$(MAKE) brand=Visa auth=EMV value=Low paynet=PAN
$(MAKE) brand=Visa auth=EMV value=High paynet=PAN
#DDA mode
$(MAKE) brand=Visa auth=DDA value=Low paynet=PAN
$(MAKE) brand=Visa auth=DDA value=High paynet=PAN

fix:
$(MAKE) paynet=PAN softfix=Yes
$(MAKE) paynet=PAN hardfix=Yes

html: #write results in HTML format
./tools/collect models-n-proofs/contact/ --output=results-contact.html #--columns=tools/columns.txt --tex-add=tools/tex-add.txt
./tools/collect models-n-proofs/contactless/ --output=results-contactless.html #--columns=tools/columns.txt --tex-add=tools/tex-add.txt
./tools/collect $(dir) #--columns=tools/columns.txt --tex-add=tools/tex-add.txt

.PHONY: clean

Expand Down

0 comments on commit 5327896

Please sign in to comment.