In recent years, credit cards have become one of the most popular payment instruments. Their growing popularity has brought many companies to store the card information of its customers. Any company that stores credit card data is subject to an international standard: PCI DSS. These stringent requirements led to consider a new method for storage and transmission of the card information: instead of protecting the actual card data, it is easier to remove and replace it with another value, called token. The substitution process is called Tokenization. In this talk, we will speak about the most signicant PCI DSS security requirements that the companies wishing to design a Tokenization algorithm must comply with, and we will present a cryptographic algorithm based on algebraic properties of cryptographic primitives. Finally we will state and prove our theorem that gives the formal security of the algorithm and implies its security within the PCI framework.