Efficient Representation of the Attacker's Knowledge in Cryptographic Protocols Analysis