Towards a Formal Verification of the Trusted Platform Module