This repository contains a Tamarin model of Oblivious HTTP.
The main model is found in ohttp.m4, and can be built with:
make
The model can be explored in Tamarin's interactive prover by running:
tamarin-prover interactive .Proofs are stored in the proofs folder, and can be rechecked with:
make proofs
or alternatively explored in the interactive prover by running
tamarin-prover interactive proofs/
You can verify the proofs non-interactively by running:
$ tamarin-prover --prove proofs/OHTTP.spthy [...] ============================================================================== summary of summaries: analyzed: OHTTP.spthy MsgSources (all-traces): verified (53 steps) end_to_end (exists-trace): verified (66 steps) ss_match (all-traces): verified (9 steps) secret_request (all-traces): verified (37 steps) secret_response (all-traces): verified (50 steps) secret_cid (all-traces): verified (6 steps) request_binding (all-traces): verified (2 steps) consistency (all-traces): verified (72 steps) reach_nonce_reuse (all-traces): verified (85 steps) ==============================================================================
The proofs were generated using the develop version of Tamarin:
tamarin-prover 1.7.0, (C) David Basin, Cas Cremers, Jannik Dreier, Simon Meier, Ralf Sasse, Benedikt Schmidt, ETH Zurich 2010-2020
Git revision: 51ab611883cc99f07967d46fe6fb5b2686dbdf24, branch: develop