Verifying a Structured Peer-to-Peer Overlay Network: The Static Case