[Teep] Formal verification of TEEP(+SUIT)

[Muhammad Usama Sardar <[e-mail]>]

Hi Akira, Okuda, chairs and all,

There are a few reasons for writing this email, including:

  * In a meeting with Hannes, Cory and Okuda during Hackathon on Sunday,
    I thought we all agreed that the properties are NOT yet verified.
  * In the TEEP meeting yesterday, I tried to repeat my concern. TEEP
    meeting notes mention that we were arguing but it does not capture
    the key technical point of argument.

Despite all above discussions, it somehow bothers me that the repo 
(https://github.com/tetsuya-okuda-hco/public-teep-formal-verif#what-is-verified-here) 
still says:

  * (DONE)
      o The authentication of TEEPAgent is verified.
      o The secrecy of encrypted payload is verified.

*/My proposed next steps/:*

As I briefly mentioned in the GitHub issue 
(https://github.com/tetsuya-okuda-hco/public-teep-formal-verif/issues/1), 
I will suggest to follow a systematic methodology for verification, 
where the first step is to create:

  * an informal protocol description detailing the steps
      o for inspiration, see this
        https://github.com/CCC-Attestation/formal-spec-TEE/blob/a836b408c385d2fd3961cc9540ee229fc3c681ca/TDX/TDX.pv#L208-L415
  * a message sequence diagram mentioning:
      o which entities are trusted
      o which channels are secure
      o what is the pre-knowledge of the entities at the start of the
        protocol
          + for inspiration, see this
            https://github.com/CCC-Attestation/formal-spec-TEE/blob/main/TDX/TDXFlowv10.pdf
              # Untrusted entities are in red
              # All channels are labelled secure/insecure
              # Pre-knowledge of the entities is shown within the boxes
                at the top

This step is an extremely valuable and crucial step as it provides a way 
to communicate with those who are not familiar with formal verification, 
specially for the designers to understand what you are going to model. 
Often the specification in IETF drafts are too vague that there are 
several revisions in this step. Once the designers agree that informal 
protocol description captures their intent, then you may proceed with 
the verification with ProVerif.

The above step will also help me understand what is the actual value of 
the proposed TEEP protocol (sorry I will not have the time to read 74 
pages draft until tomorrow). From the ProVerif artifacts, I see that at 
the beginning of the protocol, both the "TAM_process" and 
"TEEP_Agent_process" are already preconfigured with the authentic public 
keys of each other. Was this intentional? If yes, isn't it a trivial 
verification problem (given that you have marked it as DONE) even if we 
set aside the reachability issue?

*/My main concern/ (on properties marked as DONE):*

Regarding "cannot be proved", I will suggest you to have a look at 
section 3.3.1 of the ProVerif manual 
(https://bblanche.gitlabpages.inria.fr/proverif/manual.pdf). Reproducing 
the text here:

    RESULT [Query] cannot be proved: This is a “don’t know” answer.
    ProVerif could not prove that the query is true and also could not
    find an attack that proves that the query is false.

Unless we ensure that the "TEEP_Agent_process" is able to decrypt the 
message successfully, it doesn't make much sense to verify the secrecy. 
Hence, you should first prove the reachability just after this line 
https://github.com/tetsuya-okuda-hco/public-teep-formal-verif/blob/0b831378cd71003eee9788e752b740812912a543/TEEP_20231003_13_1.pv#L198. 
Note here that the reachability at Horn clauses level (as you were 
showing in Hackathon) is not enough. The reachability should hold at the 
applied pi-calculus level. See Chapter 2 of ProVerif manual, in 
particular the ending. Reproducing the text here:

    *(The authors remark that writing code with unreachable points is a
    common source of errors for new users. Advice on avoiding such
    pitfalls will be presented in Section 4.3.1.)*

So please read Section 4.3.1 and hopefully my concern should be clear to 
you then. Otherwise I am here until tomorrow evening, and will be happy 
to discuss further if there is need.


Cheers,

Usama