Skip to content

online-payment-tamarin/online-payment-security

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

3 Commits
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Modeling the Security of Online Payment Protocols

This is the support source code for the Modeling the Security of Online Payment Protocols anonymous submission to IEEE S&P 2021.

Prerequisites

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

Installation

git clone https://github.com/online-payment-tamarin/online-payment-security

Structure

  • 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

Configs and Running

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

Lemmas

sanity-check

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

validate-shown-price

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

merchant-replays-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

intercept-card-data

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_number can not be guaranteed
  • Holds -> the man in the middle can't intercept sensitive card information

hijack-transaction

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.

forge-payment-processor-confirmation

Description:

  • This lemma checks if a Check_merchant_received_confirmation() can happen without a Check_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

forge-merchant-confirmation

Description:

  • This lemma checks if a Check_transaction_approved() can happen without a Check_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

client-tampers-price

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

mitm-tampers-price

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

merchant-tampers-price

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

About

Modeling the Security of Online Payment Protocols

Topics

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published