TAMARINDIR=~/.local
TAMARINEXE=${TAMARINDIR}/bin/tamarin-prover

LEMMATA = soundness correctness secrecy connection

########################
## Single check examples
LEMMA=soundness

########################
## output/interactive
TYPE=--prove --output=localpki_${@}.log 
#TYPE=interactive

########################
## define to attack the protocol with some leaked key
## ex: make ATTACK=-Dleakltklra secrecy
ATTACK=
#ATTACK=-Dleakltken
#ATTACK=-Dleakltklra
#ATTACK=-Dleakltkalice
#########################

#########################
## Multiple threads
ifdef THREADS
NUMTHREADS=+RTS -N${THREADS} -RTS
else
NUMTHREADS=
endif
#########################


all: ${LEMMATA}

SRCTAMARIN=localpki.spthy

define runtamarin
	${TAMARINEXE} ${TYPE} -D${LEMMA} ${ATTACK} ${NUMTHREADS} ${SRCTAMARIN}
endef	

.PHONY:${LEMMATA}

soundness: LEMMA=soundness
correctness: LEMMA=correctness
secrecy: LEMMA=secrecy
connection: LEMMA=connection

soundness: ${SRCTAMARIN}
	$(call runtamarin)

correctness: ${SRCTAMARIN}
	$(call runtamarin)

secrecy: ${SRCTAMARIN}
	$(call runtamarin)

connection: ${SRCTAMARIN}
	$(call runtamarin)