Computationally Sound Symbolic Secrecy in the Presence of Hash Functions