Many recent analyses for conventional imperative programs begin by transforming programs into logic programs, capitalising on existing LP analyses and simple LP semantics. We propose using logic programs as an intermediate program representation throughout the compilation process. With restrictions ensuring determinism and single-modedness, a logic program can easily be transformed to machine language or other low-level language, while maintaining the simple semantics that makes it suitable as a language for program analysis and transformation. We present a simple LP language that enforces determinism and single-modedness, and show that it makes a convenient program representation for analysis and transformation.

Secure updates in a peer-to-peer game where all of the players are untrusted offers a unique challenge. We analyse the NEO protocol which was designed to accomplish the exchange of update information among players in a fair and authenticated manner. We show that of the five forms of cheating it was designed to prevent, it prevents only three. We then propose an improved protocol which we call Secure Event Agreement (SEA) which prevents all five types of cheating as well as meeting some additional security criteria. We also show that the performance of SEA is at worst equal to NEO and in some cases better.