Formal Methods in Security

Vassena, 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
Modeler: PersonA and PersonB
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 timetable.

Tools:

  • Use rocket chat to ask questions, e.g., ambiguity in the specification.
  • ProVerif is the recommended tool, but Tamarin is supported, too (and gets an implicit bonus for the additional research). If you want to use other tools: talk to me. 
  • For teams: create a repository at github.com or on projects.cispa.de (if you have access) and grant me (read) access.

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: name your team like the 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.

UPDATE: the team grouping feature in the CMS does not permit choosing the name of the team. So let's manifest the assignment as follows: in the RocketChat channel #proto, add a "discussion" (plus-sign next to the text box) with the name of your favorite project. In case of a conflict, we will resolve the conflict in that discussion. It also serves as a hub for questions that you might have.

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. Model the steps "Creating the account" and "Login: ..". Model PBKDF2, HKDF and scrypt like you would model hash functions.
    2. Formulate authentication.

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.