Title: Formal Model of Asynchronous Communication and Its Use in Mechanically Verifying a Biphase Mark Protocol