#!/bin/sh

##Please update to correspond to the location of ProVerif/CryptoVerif on your computer
TIMER=$HOME/xtime
PROVERIF=$HOME/proverif1.96/proverif
CRYPTOVERIF="$HOME/cryptoverif1.26/cryptoverif -lib ../../arinc823"

if [ -x $TIMER ]
then
    PROG=$TIMER
else
    PROG=
fi

## Build the library of primitives for CryptoVerif

cat $HOME/dev/cryptoverif/default.cvl arinc823prim.cvl > arinc823.cvl

## Analysis of the shared-key protocol, in ProVerif

cd sharedkey/symbolic

(
for prop in AUTHENTICATION SECRECY KEY_SECRECY UKS   
do

for enc in ENC_SUPPORTED ENC_NOTSUPPORTED
do

for speed in FAST #SLOW
do
echo PROTOCOL shared-key PV $prop.$enc.$speed

m4 -D$prop -D$enc -D$speed arinc823-secret-key.m4.pv > arinc823-secret-key.$prop.$enc.$speed.pv
$PROG $PROVERIF arinc823-secret-key.$prop.$enc.$speed.pv > arinc823-secret-key.$prop.$enc.$speed.result
egrep '(RESULT|goal reachable)' arinc823-secret-key.$prop.$enc.$speed.result
grep system arinc823-secret-key.$prop.$enc.$speed.result | grep user

done
done
done

) | tee results

## Analysis of the shared-key protocol, in CryptoVerif

cd ../computational

(
for prop in SECRECY AUTHENTICATION UKS KEY_SECRECY 
do

for prot in ORIGINAL SINGLE_TU REPLAY_PROT
do

echo PROTOCOL shared-key CV $prop.$prot

file=arinc823-secret-key.$prop.$prot
m4 -D$prop -D$prot arinc823-secret-key.$prop.m4.cv > $file.cv
$PROG $CRYPTOVERIF $file.cv > $file.result < /dev/null
egrep '(RESULT Could|All queries proved)' $file.result
grep system $file.result | grep user

done
done
) | tee results

## Analysis of the public-key protocol, in ProVerif

cd ../../publickey/symbolic

# The arguments of analyze are
# $1 = property
# $2 = compromise status
# $3 = encryption or not
# $4 = fast (without encode(encode_OFF, x) = x and compress(comp_OFF, x) = x) or slow (with it)

function analyze()
{
echo PROTOCOL public-key PV $1.$2.$3.$4

file=arinc823-public-key.$1.$2.$3.$4

m4 -D$1 -D$2 -D$3 -D$4 arinc823-public-key.m4.pv > $file.pv
$PROG $PROVERIF $file.pv > $file.result
egrep '(RESULT|goal reachable)' $file.result
grep system $file.result | grep user
}

(
for prop in SECRECY AUTHENTICATION KEY_SECRECY
do
for enc in ENC_SUPPORTED ENC_NOTSUPPORTED
do
for speed in FAST #SLOW
do
analyze $prop NO_COMPROMISE $enc $speed
done
done
done

analyze SECRECY PFS ENC_SUPPORTED FAST
analyze KEY_SECRECY PFS ENC_SUPPORTED FAST
analyze AUTHENTICATION COMPROMISE_U ENC_SUPPORTED FAST
analyze AUTHENTICATION COMPROMISE_V ENC_SUPPORTED FAST

) | tee results

## Analysis of the public-key protocol, in CryptoVerif

cd ../computational

function analyzecv()
{
echo PROTOCOL public-key CV $1

$PROG $CRYPTOVERIF arinc823-public-key.$1.cv > arinc823-public-key.$1.result < /dev/null
egrep '(RESULT Could|All queries proved)' arinc823-public-key.$1.result
grep system arinc823-public-key.$1.result | grep user
}

(
# Analyze the original protocol

for i in NOREPLAY_PROT REPLAY_PROT
do

    for j in SECRECY AUTHENTICATION KEY_SECRECY
    do
    
	m4 -D$i arinc823-public-key.$j.m4.cv > arinc823-public-key.$j.$i.cv
	analyzecv $j.$i

    done

done

# Analyze the fixed protocol

for j in REPLAY_PROT #NOREPLAY_PROT 
do

m4 -D$j arinc823-public-key.fixed.KEY_SECRECY.m4.cv > arinc823-public-key.fixed.KEY_SECRECY.$j.cv
analyzecv fixed.KEY_SECRECY.$j

m4 -D$j arinc823-public-key.fixed.SECRECY.m4.cv > arinc823-public-key.fixed.SECRECY.$j.cv
analyzecv fixed.SECRECY.$j

for k in COMPROMISE_U COMPROMISE_V NO_COMPROMISE
do 

m4 -D$j -D$k arinc823-public-key.fixed.AUTHENTICATION.m4.cv > arinc823-public-key.fixed.AUTHENTICATION.$k.$j.cv
analyzecv  fixed.AUTHENTICATION.$k.$j

done
done

) | tee results

## Build the full summary

cd ../..

(
echo SHARED KEY PROTOCOL
echo
egrep '(PROTOCOL|RESULT|system)' sharedkey/symbolic/results
echo
egrep '(PROTOCOL|RESULT Could|All queries proved|system)' sharedkey/computational/results
echo
echo PUBLIC KEY PROTOCOL
echo
egrep '(PROTOCOL|RESULT|system)' publickey/symbolic/results
echo
egrep '(PROTOCOL|RESULT Could|All queries proved|system)' publickey/computational/results
 
) | tee results