Formally Reasoning About Security Issues In P2P Protocols: A Case Study