--------------------------------------------------------------------------------
--
--  Murphi Model of An Anonymous Electronic Voting Protocol for Voting Over The Internet
--
--------------------------------------------------------------------------------
--This version by Paul Valiant, based on similar code by Dale Neal and
--Garrett Smith
--
-- Assumptions: See the writeup
--
--------------------------------------------------------------------------------



--------------------------------------------------------------------------------
-- constants, types and variables
--------------------------------------------------------------------------------


-- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
const
  NumBDs:   1;   -- number of Ballot Distributors
  NumCAs:   1;   -- number of Certification Authorities
  NumVCs:   1;   -- number of Vote Counters
  NumGoodVoters: 2; -- number of Voters
  NumBadVoters: 4; -- number of unregistered and fake voters we have to
	          -- play with
  NetworkSize:     1;   -- max. number of outstanding messages in network
  MaxVotes:   6;   -- max. number of votes allowed in system
  TrustworthyBD: FALSE;
  TrustworthyCA: FALSE;  --whether each of these agents is trustworthy
  TrustworthyVC: FALSE;
  VoterVerification: TRUE;--whether the voters or the "authorities" verify
                           --the election

-- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
type
  BDId:  scalarset (NumBDs);
  CAId:  scalarset (NumCAs);
  VCId:  scalarset (NumVCs);
  GoodVoterId: scalarset (NumGoodVoters);
  BadVoterId: scalarset (NumBadVoters);
  VoterId:  union {GoodVoterId, BadVoterId};
  
  AgentId:      union {BDId, CAId, VCId, GoodVoterId, BadVoterId};

  MessageType : enum {           -- different types of messages
    M_BlankBallotDistribution,
    M_VoterCertification_a,
    M_BadVoterCertification,--if a bad voter knows he has a cooperative 
      --CA, he'll send a special message omitting any voter certification.
    M_VoterCertification_b,
    M_VoteCasting_a,
    M_VoteCasting_b,
    M_VoteCasting_c,
    M_VoteCasting_d
  };

  BlankBallot : record  -- encrypted for voterId
    serialNo: AgentId;  -- AgentId of voter  [y]
    signingKey: AgentId;  -- Key signing serial number (BD's) [h(y), BDd]
    voterId: AgentId;  -- AgentId of voter [h(voter certificate), BDd]
  end;

  VoterCertification_a : record -- V -> CA
    saltedMark: AgentId; -- mx[r,CAe] 
    saltedMarkSignature: AgentId; -- [h(mx[r,CAe]), Vd]
    voterId: AgentId; -- [{V, voter-certificate, [h(voter-certificate), BDd]} CAe]
  end;

  BadVoterCertification : record -- V -> CA
    saltedMark: AgentId; -- mx[r,CAe] 
    saltedMarkSignature: AgentId; -- [h(mx[r,CAe]), Vd]
  end;
 
  VoterCertification_b : record -- CA -> V
    saltedSignedMark: AgentId; -- [{mx[r, CAe]}, CAd]
    signingKey: AgentId;
  end;

  VoteCasting_a : record -- V -> VC
    vote: boolean; -- vote yes/no. Good people vote yes, bad peopel vote no
    signedMark: AgentId -- [m, CAd]
  end;

  CAInfo : record
    cert : AgentId; --was:VoterCertification_a;
    response : boolean;
  end;



  Message : record
    source:   AgentId;           -- source of message
    dest:     AgentId;           -- intended destination of message
    key:     AgentId;           -- public key used for signing
    mType:    MessageType;       -- type of message
    blankBallot: BlankBallot;
    voterCertification_a: VoterCertification_a;
    badVoterCertification: BadVoterCertification;
    voterCertification_b: VoterCertification_b;
    voteCasting_a: VoteCasting_a;
  end;

  -- remark: keys, nonces and addresses are encoded in the message by their
  --         agent's identifier only. They can be distinguished by their po-
  --         sition and the type of the message

  VoterStates : enum {
    V_SLEEP,
    V_HAS_BALLOT,
    V_CERTIFY_WAIT,
    V_HAS_CERTIFICATION,
    V_VOTED
  };

  Voter : record
    state: VoterStates;
    ballotSerial: AgentId;
    ballotSigner: AgentId;
    signedMark: AgentId;
    markSigner: AgentId;
  end;

  VC : record
    votes: multiset[MaxVotes] of VoteCasting_a;  -- recorded votes
  end;

  CA : record
    certifications: multiset[MaxVotes] of CAInfo; -- received blinded voters marks
  end;

  BD : record
    serialNumbers: array[VoterId] of boolean; -- serial numbers issued
  end;  


-- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
var                                         -- state variables for
  net: multiset[NetworkSize] of Message;    --  network
  bd: array[BDId] of BD;
  ca: array[CAId] of CA;
  vc: array[VCId] of VC;
  voter: array[VoterId] of Voter;


--------------------------------------------------------------------------------
-- rules
--------------------------------------------------------------------------------

--------------------------------------------------------------------------------
-- Step 1 of the protocol
--------------------------------------------------------------------------------

ruleset i: GoodVoterId do
  ruleset j: BDId do
    rule 20 "BD sends ballot to good voter (1)"
      voter[i].state = V_SLEEP &
      multisetcount(l:net, true) < NetworkSize
    ==>
    var
      outM: Message; -- outgoing message
      begin
        undefine outM;
        outM.source := j;
        outM.dest := i;
        outM.key := i;
        outM.mType := M_BlankBallotDistribution;
        outM.blankBallot.serialNo := i;
        outM.blankBallot.signingKey := j;
        outM.blankBallot.voterId := i;
	   
        multisetadd (outM, net);
					      
      end;
  end;
end;


ruleset i: BadVoterId do
  ruleset j: BDId do
    ruleset k: GoodVoterId do
    rule 20 "BD sends ballot to bad voter (1)"
      !TrustworthyBD & voter[i].state = V_SLEEP &
      multisetcount(l:net, true) < NetworkSize
    ==>
    var
      outM: Message; -- outgoing message
      begin
        undefine outM;
        outM.source := j;
        outM.dest := i;
        outM.key := i;
        outM.mType := M_BlankBallotDistribution;
        outM.blankBallot.serialNo := k;  -- give the bad voter the serial number and certificate of a good voter
        outM.blankBallot.signingKey := j;
        outM.blankBallot.voterId := k;
	   
        multisetadd (outM, net);
					      
      end;
  end;
end;
end;
							
ruleset i: GoodVoterId do
ruleset k: BDId do
  choose j: net do
    rule 20 "Good voter receives ballot (1)"
      net[j].dest = i &
      net[j].mType = M_BlankBallotDistribution
      ==>
      var
        inM: Message; -- incoming message
      begin
        inM := net[j];
        multisetremove (j, net);
        if inM.key=i then --encrypted with i's key
          if inM.mType=M_BlankBallotDistribution then
	   if inM.blankBallot.signingKey = k then
	       voter[i].ballotSerial := inM.blankBallot.serialNo;
	       voter[i].state := V_HAS_BALLOT;
	       voter[i].ballotSigner := inM.blankBallot.signingKey;
	   end;
	end;
        end;
      end;
  end;
end;
end;

ruleset i: BadVoterId do
ruleset k: BDId do
  choose j: net do
    rule 20 "Bad voter receives ballot (1)"
      net[j].dest = i &
      net[j].mType = M_BlankBallotDistribution
      ==>
      var
        inM: Message; -- incoming message
      begin
        inM := net[j];
        multisetremove (j, net);
        if inM.key=i then --encrypted with i's key
          if inM.mType=M_BlankBallotDistribution then
	       voter[i].ballotSerial := inM.blankBallot.serialNo;
	       voter[i].state := V_HAS_BALLOT;
	end;
        end;
      end;
  end;
end;
end;

--------------------------------------------------------------------------------
-- Step 2 of protocol
--------------------------------------------------------------------------------

ruleset i: GoodVoterId do
  ruleset j: CAId do
    rule 20 "Voter sends certification request (2a) "
      voter[i].state = V_HAS_BALLOT &
      multisetcount(l:net, true) < NetworkSize
    ==>
    var
      outM: Message; -- outgoing message
      begin
        undefine outM;
        outM.source := i;
        outM.dest := j;
        outM.key := j;
        outM.mType := M_VoterCertification_a;
        outM.voterCertification_a.saltedMark := i;
        outM.voterCertification_a.saltedMarkSignature := i;
        outM.voterCertification_a.voterId := i;	   
        multisetadd (outM, net);
        voter[i].state := V_CERTIFY_WAIT;
      end;
  end;
end;

ruleset i: BadVoterId do
  ruleset j: CAId do
    rule 20 "Bad Voter sends certification request (2a) "
      voter[i].state = V_HAS_BALLOT &
      multisetcount(l:net, true) < NetworkSize
    ==>
    var
      outM: Message; -- outgoing message
      begin
        undefine outM;
        outM.source := i;
        outM.dest := j;
        outM.key := j;
        outM.mType := M_VoterCertification_a;
        outM.voterCertification_a.saltedMark := i;
        outM.voterCertification_a.saltedMarkSignature := i;
        outM.voterCertification_a.voterId := voter[i].ballotSerial;
        multisetadd (outM, net);
        voter[i].state := V_CERTIFY_WAIT;
      end;
  end;
end;

ruleset i: BadVoterId do
  ruleset j: CAId do						       
    rule 20 "Bad Voter asks for fraudulent certification"
      voter[i].state = V_SLEEP & --voter doesn't have to have received anything!
      multisetcount(l:net, true) < NetworkSize
    ==>
    var
      outM: Message; -- outgoing message
      begin
        undefine outM;
        outM.source := i;
        outM.dest := j;
        outM.key := j;
        outM.mType := M_BadVoterCertification;
        outM.badVoterCertification.saltedMark := i;
        outM.badVoterCertification.saltedMarkSignature := i;
        multisetadd (outM, net);
        voter[i].state := V_CERTIFY_WAIT;
      end;
  end;
end;

ruleset i: CAId do
  choose j: net do
    rule 20 "CA receives certification request (2a) "
      net[j].dest = i 
      ==>
      var
        inM: Message; -- incoming message
        info: CAInfo;
      begin
        undefine info;
        inM := net[j];
        multisetremove (j, net);
        if inM.key=i then --encrypted with i's key
          if inM.mType=M_VoterCertification_a then
	   if !TrustworthyCA |
             inM.voterCertification_a.saltedMarkSignature 
               = inM.voterCertification_a.voterId then
	     info.cert := inM.voterCertification_a.saltedMark;
	     info.response := false;
             multisetadd (info, ca[i].certifications);
	   end;
	end;
        end;
      end;
  end;
end;

ruleset i: CAId do
  choose j: net do
    rule 20 "CA accepts fraudulent certification request (3a) "
      !TrustworthyCA &
      net[j].dest = i 
      ==>
      var
        inM: Message; -- incoming message
        info: CAInfo;
      begin
        undefine info;
        inM := net[j];
        multisetremove (j, net);
        if inM.key=i then --encrypted with i's key
          if inM.mType=M_BadVoterCertification then
	     info.cert := inM.badVoterCertification.saltedMark;
	     info.response := false;
	     multisetadd (info, ca[i].certifications);
	   end;
        end;
      end;
  end;
end;

ruleset i: CAId do
  choose j: ca[i].certifications do
    rule 20 "CA responds to certification request (3b)"
      ca[i].certifications[j].response = false &
      multisetcount(l:net, true) < NetworkSize
      ==>
      var
        outM: Message; -- outgoing message
      begin
        undefine outM;
        outM.source := i;
        outM.dest := ca[i].certifications[j].cert;
        outM.key := ca[i].certifications[j].cert;
        outM.mType := M_VoterCertification_b;
        outM.voterCertification_b.saltedSignedMark := ca[i].certifications[j].cert;
        outM.voterCertification_b.signingKey := i;
        multisetadd (outM, net);
        ca[i].certifications[j].response := true;
        if (ismember(ca[i].certifications[j].cert, BadVoterId)) then
          --don't publish the marks of fake voters; under a trustworthy
          --  CA, these won't even be here.
   	  multisetremove(j, ca[i].certifications);
        end;
      end;
  end;
end;

ruleset i: GoodVoterId do
  choose j: net do
    rule 20 "Good voter recieves certification from CA (3b) "
      net[j].dest = i &
      voter[i].state = V_CERTIFY_WAIT
      ==>
      var
        inM: Message; -- incoming message
      begin
        inM := net[j];
        multisetremove (j, net);
        if inM.key = i then
          if inM.mType = M_VoterCertification_b then
	  voter[i].signedMark := inM.voterCertification_b.saltedSignedMark; 
				   -- removes the salt
          voter[i].state := V_HAS_CERTIFICATION;
	  voter[i].markSigner := inM.voterCertification_b.signingKey;
	end;
        end;
      end;
  end;
end;

ruleset i: BadVoterId do
  choose j: net do
    rule 20 "Bad voter recieves certification from CA (3b) "
      net[j].dest = i &
      voter[i].state = V_CERTIFY_WAIT
      ==>
      var
        inM: Message; -- incoming message
      begin
        inM := net[j];
        multisetremove (j, net);
        if inM.key = i then
          if inM.mType = M_VoterCertification_b then
	  voter[i].signedMark := inM.voterCertification_b.saltedSignedMark; 
				   -- removes the salt
          voter[i].state := V_HAS_CERTIFICATION;
	  voter[i].markSigner := inM.voterCertification_b.signingKey;
	end;
        end;
      end;
  end;
end;

--------------------------------------------------------------------------------
-- Step 3 of the protocol
--------------------------------------------------------------------------------
ruleset i: GoodVoterId do
  ruleset j: VCId do
    rule 20 "Voter sends vote to VC"
      voter[i].state = V_HAS_CERTIFICATION &
      multisetcount(l:net, true) < NetworkSize
      ==>
      var
        outM: Message; -- outgoing message
      begin
        undefine outM;
        outM.source := i;
        outM.dest := j;
        outM.key := j;
        outM.mType := M_VoteCasting_a;
        outM.voteCasting_a.vote := true;
        outM.voteCasting_a.signedMark := voter[i].signedMark;
        multisetadd (outM, net);
        voter[i].state := V_VOTED;
      end;
  end;
end;

ruleset i: BadVoterId do
  ruleset j: VCId do
    rule 20 "Bad Voter sends vote to VC"
      voter[i].state = V_HAS_CERTIFICATION &
      multisetcount(l:net, true) < NetworkSize
      ==>
      var
        outM: Message; -- outgoing message
      begin
        undefine outM;
        outM.source := i;
        outM.dest := j;
        outM.key := j;
        outM.mType := M_VoteCasting_a;
        outM.voteCasting_a.vote := false;
        outM.voteCasting_a.signedMark := voter[i].signedMark;
        multisetadd (outM, net);
        voter[i].state := V_VOTED;
      end;
  end;
end;

--------------------------------------------------------------------------------
-- behavior of Vote Counter

-- VC i reacts to vote received
ruleset i: VCId do
  choose j: net do
    rule 20 "VC reacts to received vote (4a) "

      net[j].dest = i
-- we don't have any explicit intruders, so we don't need to check 
-- if the message is from an intruder
    ==>

    var
      inM:  Message;   -- incoming message

    begin
      inM := net[j];
      multisetremove (j,net);

      if inM.key=i then   -- message is encrypted with i's key

        if inM.mType=M_VoteCasting_a then   -- correct message type
	   if multisetcount (l:vc[i].votes,   -- add only if not there
	         --don't want to allow someone to case multiple votes,
	         --so we should only check the voter mark for
	         --individuality
                   vc[i].votes[l].signedMark = inM.voteCasting_a.signedMark) = 0 then
                 multisetadd (inM.voteCasting_a, vc[i].votes);
           else
             --error "vote already cast"
           end;
        end;

      end;
    end;
  end;
end;

--here the VC decides to ignore someone's vote
ruleset i: VCId do
  choose j: net do
    rule 20 "VC drops a vote on the floor!"
      !TrustworthyVC &
      net[j].dest = i
      ==>
      begin
        multisetremove (j, net);
      end;
  end;
end;



--------------------------------------------------------------------------------
-- startstate
--------------------------------------------------------------------------------

startstate
  -- initialize Voters
  undefine voter;
  for i: VoterId do
    voter[i].state := V_SLEEP;
  end;

  -- initialize VCs
  undefine vc;

  -- initialize CAs  
  undefine ca;
  --for i: CAId do
  --  for j: VoterId do  
  --    ca[i].certifications[j] := false;
  --  end;
  --end;

  -- initialize BDs
  undefine bd;
  for i: BDId do
    for j: VoterId do  
      bd[i].serialNumbers[j] := false;
    end;
  end;

  -- initialize network 
  undefine net;
end;

--------------------------------------------------------------------------------
-- invariants
--------------------------------------------------------------------------------

 invariant "voter votes for who they think they do"
  forall i: GoodVoterId do
    forall j: VCId do
      voter[i].state = V_VOTED
      ->
      multisetcount (l:vc[j].votes,
                   vc[j].votes[l].signedMark = voter[i].signedMark &
                   vc[j].votes[l].vote = false) = 0
    end
  end;

  invariant "voter can prove fraud if their vote is uncounted"
    forall i: GoodVoterId do
      forall j: VCId do
        voter[i].state = V_VOTED &
        multisetcount (l:vc[j].votes,
                       vc[j].votes[l].signedMark = voter[i].signedMark) = 0
        ->
        ismember(voter[i].ballotSigner, BDId) &
        ismember(voter[i].markSigner, CAId)
      end
    end;

  invariant "a fraudulent vote can be detected by authorities"
    forall i: VCId do
      forall j: CAId do
        !VoterVerification &
        multisetcount(l:vc[i].votes,
                      vc[i].votes[l].vote = false) > 0
        ->
        multisetcount(l:vc[i].votes, true) > 
          multisetcount(m:ca[j].certifications, ca[j].certifications[m].response) 
        -- if there is a fraudulent vote, there must
        -- be more votes than published certified
        -- voters.
      end
    end;


  --invariant "a fraudulent vote can be detected by a voter"
  --I'm not sure how to implement this as an invariant, so the code below
  --is rather messy
    ruleset i: VCId do
      ruleset j: CAId do 
        rule 20 "Invariant: fraudulent vote can be detected by voter"
          VoterVerification
          ==>
          var c: 0..NumGoodVoters;
            goodsofar: Boolean;
          begin
            if multisetcount(l:vc[i].votes,
                 vc[i].votes[l].vote = false) > 0 then
               c:=0;
               goodsofar:=true;
               for k: GoodVoterId do
	         if voter[k].state=V_VOTED &
	           multisetcount(l:vc[i].votes,vc[i].votes[l].signedMark=k)=0 then
          	     goodsofar:=false;
 	         else
                   if voter[k].state=V_HAS_CERTIFICATION | 
                       voter[k].state=V_CERTIFY_WAIT then
		     c:=c+1;
		   end;
		 end;
	       end;
               if goodsofar & multisetcount(l:vc[i].votes, true)+c <= 
                      multisetcount(m:ca[j].certifications,
                      ca[j].certifications[m].response) then
                 error "Invariant violated: voters can detect a fraudulent vote"
	       end
             end
	   end;
	 end;
       end;

