This is the support source code for the Modeling the Security of Online Payment Protocols anonymous submission to IEEE S&P 2021.
Brew
sh -c "$(curl -fsSL https://raw.githubusercontent.com/Linuxbrew/install/master/install.sh)"
Tamarin-Prover
brew install tamarin-prover/tap/tamarin-prover
m4
sudo apt-get install m4
git clone https://github.com/online-payment-tamarin/online-payment-security
- classes: contains implementations of generic rules of protocols which belong in a given class
- lemmas: contains different adversarial attacks, described using lemmas
- channels: testing the protocols using different (more restrictive) channels - e.g.: enforcing confidentiality, confidentiality + authentication, etc.
- output: file generated by m4
In main.spthy, define the class of protocols that needs to be evaluated using the current set of lemmas
e.g.:
define(`direct-encrypted', 1)
will test the lemmas for the direct-encrypted class of protocols.
Experimental: you can also define the channel used for communications. I'm still testing this. Some lemmas might need to be adjusted.
e.g.:
define(`confidential-channel', 1)
will use a confidential channel; the adversary can't replay messages (since no access to these messages is provided) but can send his own messages.
Run with make
Description:
- Lemma aims to validate the functionality of the model by presuming that there is no way a transaction is approved (completed). If there exists a timestamp at which
Check_transaction_approved()happens, then there exists a method of completing a transaction. It makes the assumption that a transaction is not possible and is up to the prover to demonstrate that it is doable. - If formulated otherwise (i.e.: 'are transactions not possible with these rules?'), Tamarin chooses to not execute certain actions (e.g.: a client decides to never send banking information), so we'd get wrong results.
Result:
- Fails -> there is a way to complete transactions using the given model
- Holds -> there is no way to reach the final state of the protocol -> possible implementation error
Description:
- Lemma checks if the transaction amount ever reaches the client (so the client is informed). I found no way to model the fact that a protocol explicitly shows the client the transaction amount, so I'm considering the client knowns it if the variable reaches the client (is sent by the client to the payment processor).
- If it does, then the transaction amount must be the same as the one in
Processor_handles_transaction(), otherwise it means that the client might be charged a different amount than indicated
Result:
- Fails -> it is formally guaranteed that the amount received by the client is also the one in the transaction
- Holds -> there is no guarantee that the amount shown to the client is the one used in the final transaction
Description:
- The objective is to check if a merchant can complete 2 transactions when the client submits the banking information only once.
Result:
- Fails -> a merchant can charge the client twice
- Holds -> only one transaction is allowed
Description:
*This lemma attempts to discover if, at any point, the card details of the client can be intercepted, in unencrypted format, by an adversary with network access (MitM). It makes the assumtption that there does not exist a timestamp #i2 at which the adversary (K) learns the card_number
Result:
- Fails -> the confidentiality of the
card_numbercan not be guaranteed - Holds -> the man in the middle can't intercept sensitive card information
Description:
- This lemma attempts to perform a transaction using the adversary's merchant id. In theory, it should work against most protocols because the prover relies on intercepting the card details of the client (or even the cryptogram) and forwarding everything to the malicious merchant which can create transactions as he wishes. In other words, the adversary is believed to be a 'legit merchant' - which is not entirely correct.
Result:
- Needs to be interpreted.
Description:
- This lemma checks if a
Check_merchant_received_confirmation()can happen without aCheck_transaction_approved()- in other words, if the merchant can receive a confirmation of a successful transaction without the transaction actually happening (without involving the payment processor)
Result:
- Fails -> payment processor's confirmations can be forged and sent by an adversary
- Holds -> payment processor's confirmations can't be forged
Description:
- This lemma checks if a
Check_transaction_approved()can happen without aCheck_client_received_confirmation()- in other words, a transaction happens and the client is not informed properly
Result:
- Fails -> payment confirmations can be forged (i.e.: the client can be tricked into paying twice, by invoking a system error)
- Holds -> payment confirmations can't be forged
Description:
- Lemma checks if the client can alter the price of the transaction by comparing the merchant's defined amount with the amount known to the client (presumed altered) and the amount used in the final step of the transaction (performed on the payment processor's server).
Result:
- Fails -> the client is able to set his own transaction amount
- Holds -> the client is not able to define his own transaction amount or does not have acces to the price variable
Description:
- Checks if the mitm can alter the price of a transaction.
Result:
- Fails -> the mitm is able to set his own transaction amount
- Holds -> the mitm is not able to change the amount
Description:
- Checks if the merchant can alter the price of a transaction in a later stage, once the transaction amount was already defined.
Result:
- Fails -> the merchant is able to change the transaction amount later
- Holds -> the merchant is not able to change the amount