clarifications about ballot checking that is not a Benaloh challenge

[kiniry]

Description

A computer scientist asked via email:

If possible I'd like to get clarification on these points today. Can you explain what has replaced the Benaloh challenge?

In looking about your conops.md (and similarly on other documents), it looks like after the voter chooses "check" and does the flow through "receive ballot checking code" ... "view passkey" ... etc., they can then submit that ballot. My specific questions are:

1. How does the fact that "Passkeys Match" prove to the voter that the encrypted ballot contains the votes they intended?

2. Can the voter prove to someone else how they voted by replaying the trace (including data such as submission hash, BCA public key, randomizers, etc?
   2a. If the answer is yes, then doesn't this lose the "strong secret ballot" property of the Benaloh challenge, that even with the collusion of the voter, the voter can't prove how they voted?
   2b. If no (if for example in step 12 of "8.4 Voter Ballot Check Sequence" the randomizers are not known to the voter), then doesn't that mean the voter has to the software and cannot really repeat all the steps using independent software?

[kiniry]

Our cryptographers write:

A1. It does not, the passkeys matching are a way to protect the
randomizers from fraudulent applications acting as BCA's. You could
say that it does show that the BCA the user is interacting with really
is interacting with the system and VA, but a bad BCA could send its
passkey and then falsify other data.

A2. Replaying the trace will not prove things unless the trace
includes decrypted randomizers, in which case you are in the same boat
as a benaloh challenge application revealing them.

A2b. Ideally the choice of BCA is made amongst several possibilities,
you have to trust that at least one of the BCAs you use is correct,
but we don't think this ideal of multiple BCA's is written down in the
current documentation.