A contactless payment lets a card holder execute payment without any interaction (e.g., entering PIN or signing) between the terminal and the card holder. Even though the security is the first priority in a payment system, the formal security model of contactless payment does not exist. Therefore, in this paper, we design an adversarial model and define formally the contactless-payment security against malicious cards and malicious terminals including relay attacks. Accordingly, we design a contactless-payment protocol and show its security in our security model. At the end, we analyze EMV-contactless which is a commonly used specification by most of the mobile contactless-payment systems and credit cards in Europe. We find that it is not secure against malicious cards. We also prove its security against malicious terminals in our model. This type of cryptographic proof has not been done before for the EMV specification.