Several proofs of security for a tokenization algorithm