Formal Methods in Security

Patrignani, Nemati, Künnemann

PROTO: project

Project for part 3: Protocol Verification

Tasks

  1. Create a well-documented model from the linked information. Try to document how your modeling relates to the specification using the following format.

    (*
Protocol: FooChat
Copyright: 2022 Robert Künnemann
SPDX-License-Identifier: (GPL-3.0-or-later AND LGPL-2.0-only) 
Sources:
 [S] https://URL-to-SPEC
 [OS] https://URL-to-other-SPEC
 [OS-l] https://URL-to-other-SPEC#link-with-anchor
Footnote:
[1] long comment
*)

let Initiator = (* Defined in [3] *)
   new n_C:bitstring; (* [1, Section "Nonce selection"] *)
   out(n_c);  (* short comment that fits in this line *)
   out(n_c); (* see [1] *)

(* etc. *)

  2. Formulate security properties that you think should hold, try to give an intuition with them and, if you find attacks, describe the attack informally as a comment.

  3. Break or modify your protocol: Create a copy of your model file and describe an interesting modification to the protocol. An interesting modification:

    • breaks a security property because it removes an important element of the protocol, e.g., an important nonce.
    • removes superfluous elements of the protocol, even if they have additional functions beyond security and the main functionality. 
    • is not completely trivial, e.g., just outputting the key in the plain.

    The bar to meet this requirement will not be set very high – this part is educational. 

Deadlines

There are two deadlines, an early and a late deadline. They are specific dates that you find in the calendar.

Tools:

  • Create a subdirectory in "proj" the repository: https://cms-gitlab.cispa.de/kuennemann/fms2021-proto-proj.
  • Use Askbot to ask questions, e.g., ambiguity in the specification.
  • ProVerif is the recommended tool.
  • Deepsec is supported and uses almost the same input language as ProVerif
  •  Tamarin is supported, too (and gets an implicit bonus for the additional research)
  • If you want to use other tools: talk to me. 

Grading

30 points in total, with the following guide values.

  • 15: An adequate model with errors and a security property that exhibits a reasonable intention gives a pass.
  • 20: Largely correct model, but close to trivial. A relevant security property was shown.
  • 25: Like 3.0, but fully correct or complex
  • 30: A more-than-trivial model that is almost completely correct and has some interesting security property shown.
  • Modifiers:
    • good documentation: -6 to +6
    • extra features: +2 to +5 depending on feature
    • elegant modeling: +5
    • participation in discussion: +2 to +5

Teamwork

Two-person teams are encouraged, but the expectation for complexity is higher. Git history will be used to review if both participants contributed equally.

Some projects have dependencies. Hence there are two deadlines: an early and a late deadline (see timetable). If the team for the prerequisite fails, the follow-up project has to start from scratch or switch to the prerequisite project.

To give you an idea of the expected complexity: if TLS was one of the possible projects and a two-person team abstracts it to the point where they arrive at BabyTLS (plus authentication properties for honest parties), then I'd be perfectly happy with that. I am thinking about 10hs of work per person, assuming you understood the lectures already and handled the exercises well.

Assignment

We use the CMS'es team grouping feature for the assignment. Please tell me via mail which protocol you want to tackle. (If you are on you own, you are a team of one.) Conflicts, i.e., two teams wanting to tackle the same project, are resolved as follows:

  • Assignment deadline closes with the last lecture. You can signup for a project afterwards, but all conflicts are resolved to the team that was created before the deadline.
  • If a team was created one week before the other, it wins out.
  • Otherwise, a coin toss decides.

Licensing

We would like to reuse the model you create in this project for future projects. Copyright (Urheberrecht, more precisely) for project work in lectures is a difficult thing and I am not a lawyer. So I ask you kindly to put your work under the GPL by following the above template, declaring your copyright and the machine-readable licence identifier "SPDX-License-Identifier: (GPL-3.0-or-later AND LGPL-2.0-only)". This is not mandatory, of course, but appreciated.

Protocols

DNSCRYPT v2

  • SOURCE: https://dnscrypt.info/protocol/
  • Deadline: early
  • Methodology: straightforward

DNS Queries over HTTPS

  • SOURCE: https://www.rfc-editor.org/rfc/rfc8484.txt
  • Deadline: early or late
  • Methodology: 
    1. Build on babytls.pv (Will be provided.)
    2. Add record protocol (simple encryption with key).
    3. Add [data]-constructors to model HTTP(S) queries and responses
    4. Model mentioned RFC.

Anonymized DNSCrypt

  • SOURCE: https://github.com/DNSCrypt/dnscrypt-protocol/blob/master/ANONYMIZED-DNSCRYPT.txt
  • Deadline: early or late
  • Builds-on: DNSCRYPT v2

DNSSEC

  • SOURCE: https://en.wikipedia.org/wiki/DomainNameSystemSecurityExtensions (links to RFC)
  • Builds-on: symsoundmodel.pv. Alexander Dax designed a model consisting of DNSSEC and SSMTP. This project consists in simplifying this model (for educational purposes).
  • Deadline: early
  • Methodology:
    1. Simplify Alex's model so that it contains only DNSSEC and the root server set-up is easier visible.
    2. Simplify authentication property.
    3. Allow for arbitrarily many root servers.
    4. Try to support arbitrary depth of resolution (i.e., domains with on.two.three. separators). Demonstrate, where it fails.

DNSSEC, arbitrary depth resolution

  • SOURCE: https://en.wikipedia.org/wiki/DomainNameSystemSecurityExtensions (links to RFC)
  • Builds-on: DNSSEC
  • Deadline: late
  • Methodology:
    1. Formulate authentication property as a chain of properties: Instead of saying: for each response to a client's query, the domain was registered before, break that property down to each request: "If client queries domain d, he learns the IP of d, or the authoritative nameserver for d"
    2. Show: "If ns is the authoritative nameserver for d, then any query to ns for the IP of d returns the IP."

DP-3T

  • SOURCE: https://blog.symbolic.software/2020/04/05/dp-3t-verifpal/
  • SOURCE: In case of doubt consult: https://github.com/DP-3T/documents
  • Deadline: early or late
  • Methodology:
    1. Create a simple model of DP-3T based on Georgio Nicolas's VerifPal model: https://blog.symbolic.software/2020/04/05/dp-3t-verifpal/
    2. (If team consists of two people)
      1. use a private channel to model that two phones can only communicate if they are in proximity
      2. extend the authentication property to show that a phone can only receive a warning message if there was a phone that (a) the health authority marked as infected and (b) both were in proximity.

Andrew Secure RPC

  • SOURCE: http://www.lsv.fr/Software/spore/andrew.html
  • Deadline: early or late
  • Methodology:
    1. Model this protocol.
    2. Discover the claimed attack.
    3. Fix the claimed attack.

Firefox Accounts/Sync Protocol

  • SOURCE: https://github.com/mozilla/fxa-auth-server/wiki/onepw-protocol
  • Deadline: early or late
  • Methodology:
    1. You build on the model `onepwprotocol.pv` which models the steps "Creating the account" and "Login: .." in the spec.
    2. Model the session token
    3. Model the steps "Signing Certificates" and "Fetching Sync Keys".
    4. Use test queries to see if the "Typical Client Flows" for creating accounts and adding new devices can be produced.
    5. Formulate authentication properties.

Megaolm

  • SOURCE: https://gitlab.matrix.org/matrix-org/olm/blob/master/docs/megolm.md
  • Deadline: early or late
  • Methodology:
    • Model a simplified ratchet consisting of only a single hash function
    • Model Ed25519 as a signature scheme
    • Model the secure peer-to-peer channel provided by olm with an asymmetric encryption scheme
    • Use ProVerif's table feature (see manual) to store the ratchet data
    • Formulate secrecy as a game where the attacker tries to guess the ratchet value without receiving an invitation to the channel
    • If necessary, restrict the counter i to three values.

Universally composable commitment protocol

  • SOURCE: Yehuda Lindell. “Highly-Efficient Universally-Composable Com- mitments Based on the DDH Assumption”. In: Advances in Cryp- tology – EUROCRYPT 2011. Ed. by Kenneth G. Paterson. Berlin, Heidelberg: Springer Berlin Heidelberg, 2011, pp. 446–466.
  • Deadline: early or later
  • Methodology:
    • Read up on the high-level idea of universal composability, e.g., here https://eprint.iacr.org/2013/062
    • Model the protocol and simulator from Lindell's proof in template file I give you
    • Show universal composability or show flaw in proof or proof technique

Wildcard examples:

  • SOURCE: https://github.com/tamarin-prover/tamarin-prover/tree/develop/examples but NOT subdirectory SAPIC
  • Deadline: early or late
  • Methodology:
    1. Translate one of these examples into ProVerif's input language
    2. Translate the security property into correspondence queries. If they involve K() or KU() facts, these need special care: they denote an adversary deducing a message. Please consult me before attempting to translate.
Privacy Policy | Legal Notice
If you encounter technical problems, please contact the administrators.