Proving Hybrid Protocols Correct
Proceedings of 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'01).
We describe a generic switching protocol for the construction of hybrid protocols and prove it correct with the Nuprl proof development system. For this purpose we introduce the concept of meta-properties and use them to formally characterize communication properties that can be preserved by switching. We also identify switching invariants that an implementation of the switching protocol must satisfy in order to work correctly.
bibTex ref: BKVL01