Payments through cards have become very popular in today\'s world. All businesses now have options to receive payments through this instrument, moreover most organizations store card information of its customers in
some way to enable easy payments in future. Credit card data is a very sensitive information and theft of this data is a serious threat to any company. Any organization that stores credit card data needs to achieve payment card industry (PCI) compliance, which is an intricate process where the organization needs to demonstrate that the data it stores is safe. Recently there has been a paradigm shift in treatment of the problem of storage of payment card information. In this new paradigm instead of the real credit card data a token is stored, this process is called ``tokenization\". The token resembles the
credit/debit card number but is in no way related to it. This solution relieves the merchant from the burden of PCI compliance in several ways.
Though tokenization systems are heavily in use, to our knowledge, a formal cryptographic study of this problem has not yet been done. In this paper we initiate a study in this direction. We formally define the syntax of a tokenization system, and several notions of security for such systems. Finally, we provide some constructions of tokenizers and analyze their security in the light of our definitions.