We present an approach to provide a fault-tolerant and secure service for sealed-bid auctions. The solution is designed for a loosely coupled publish/subscribe system. It employs multiple auction servers and achieves validity and security properties through application of secret-sharing methods and public-key encryption and signatures. It can tolerate Byzantine failures of one third of the auction servers and any number of bidders. A verification of the desired properties has been machine-checked using PVS. This work also provides insight and useful experience in techniques for specifying and verifying this type of system.

• dcca8.ps