#!/usr/bin/env perl

use strict;
use warnings;

use Getopt::Long;

# argument processing
my $votingserver=0;
my $registrar=0;

sub conv {
    my ($o,$s)=@_;
    if ($s eq '0' || $s eq 'honest') {return 0;}
    if ($s eq '1' || $s eq 'dishonest') {return 1;}
    die "bad option $o: $s, stopped";
}

GetOptions ('votingserver|s=s' => sub {$votingserver=conv(@_);},
            'registrar|r=s' => sub {$registrar=conv(@_);})
    or die;

my $cast_as_intended_id = "";
my $indverif_id = "";
my $cast_as_intended_cred = "";
my $indverif_cred = "";
my $check = "";

while (<>) {
    if (/RESULT event\(VERIFIED.* ==> event\(VOTE.* (is true|is false|cannot be proved)\./) {        
        $check = $1;
    }
    if (/RESULT event\(VERIFIED.* ==> event\(GOING_TO_TALLY.* (is true|is false|cannot be proved)\./) {        
        $indverif_id = $1;
    }
    if (/RESULT event\(VERIFIED.* ==> \(event\(VOTER.* (is true|is false|cannot be proved)\./) {        
        $indverif_cred = $1;
    }
    if (/RESULT event\(GOING_TO_TALLY\(([^,]*),([^,]*),.* ==> .*event\(VOTER\(([^,]*),([^,]*),H.* (is true|is false|cannot be proved)\./) {        
        if ($1 eq $3) {
            $cast_as_intended_id = $5;
        }
        if ($2 eq $4) {
            $cast_as_intended_cred = $5;
        }
    }
}

if ($check eq "" || $indverif_id eq "" || $indverif_cred eq "" || $cast_as_intended_id eq "" || $cast_as_intended_cred eq "") {
    die "unable to parse proverif output correctly."
}

if ($check ne "is true") {
    die "honest voter behaviour is not proved."
}


if (($votingserver==0 && $indverif_id eq "is true" && $cast_as_intended_id eq "is true") || ($registrar==0 && $indverif_cred eq "is true" && $cast_as_intended_cred eq "is true")) {
    print "verifiable.\n";
} else {
    if (($votingserver==0 && ($indverif_id eq "is false" || $cast_as_intended_id eq "is false")) || ($registrar==0 && ($indverif_cred eq "is false" || $cast_as_intended_cred eq "is false"))) {
        print "not verifiable.\n";
    } else {
        if ($votingserver==1 && $registrar==1) {
            print "both authorities dishonest.\n";
        } else {
            print "cannot be proved.\n";
        }
    }
}
#print "check ".$check." ivid ".$indverif_id." caiid ".$cast_as_intended_id." ivcred ".$indverif_cred." caicred ".$cast_as_intended_cred."\n";
