Re: [Teep] Formal verification of TEEP(+SUIT)

[Okuda Tetsuya <[e-mail]>]

Dear Usama,

I'm sorry for bothering you due to the delayed response.
I was so busy this week, so I thought I would revise the description
this weekend.
I have just revised the description on the repository in accordance with
the slides.
I have also clarified the status of this project as training.

Yes, I think I should follow the methodologies as you suggested.
In addition, I reconsider the reachability property at the applied
pi-calculus level,
  even if I have examined carefully at the horn-clause level.
Thank you for offering detailed advice.

Best regards,
Okuda Tetsuya

2023年11月9日(木) 19:08 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)
>       - The authentication of TEEPAgent is verified.
>       - 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
>       - for inspiration, see this
>       https://github.com/CCC-Attestation/formal-spec-TEE/blob/a836b408c385d2fd3961cc9540ee229fc3c681ca/TDX/TDX.pv#L208-L415
>    - a message sequence diagram mentioning:
>       - which entities are trusted
>       - which channels are secure
>       - 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
>
> _______________________________________________
> TEEP mailing list
> [e-mail]
> https://www.ietf.org/mailman/listinfo/teep
>