fare
commented
5 years ago I'm not sure how to feasibly quantify over programs with Z3; probably "not".
Instead, we should probably focus on the "knowability theory" of some cryptographic expression depending on a context of known expressions—that's a typical logical "provability" theory, hopefully small and decidable, that can be made into a Z3 SMT extension. Then, we can prove whether or not "Bob knows Alice's hand" given the information available at a given point in the program, and we can have a separate proof that Bob has a winning strategy if and only if he knows Alice's hand.
The property would be something like: "there exists a winning strategy for Bob". i.e. at the point in the program where Bob makes his choice, there is a pure function that abstracts over the cryptographic primitives, such that if Bob uses this function to make his choice, he will always win.
That's a second order predicate (abstracts over that function that Bob uses), though, the function being pure and simple, could be represented as a first-order entity by its source in some minimal grammar. Still quite a heavy predicate to express, even more so to prove: it's easy to exhibit the winning strategy in the non-committed case, though it might not be trivial to find it affordably through search; it could be hard to prove the absence of winning strategy in the committed case.