search

CCC-Attestation / governance

Apache License 2.0
0 stars 5 forks source link

attested TLS POC #7

Closed thomas-fossati closed 1 year ago

thomas-fossati commented 2 years ago

Background material

Previous relevant Attestation SIG presentations:

Date Track Presentation Presenter Materials
2022-08-02 secure channel establishment A TLS+CWT (v2) implementation in mbedTLS Ionut Mihalcea (@ionut-arm) & Thomas Fossati (@thomas-fossati) slides
2022-04-26 secure channel establishment TLS + CWT Hannes Tschofenig (@hannestschofenig) slides IETF draft

Proposal

A POC end-to-end demo integrating veraison, mbedTLS and PARSEC to implement the following (work-in-progress) specifications:

Proponents

muhammad-usama-sardar commented 2 years ago

TLS extensions to support attestation as first-class authentication credentials

Background

See the presentation of Tom Roeder on 2022-03-29 for the importance of formal specification and verification of protocols

Proposal

Formal specification and verification of proposed TLS extensions in state-of-the-art symbolic security analysis tool ProVerif making use of the existing verification of TLS

Proponents

KeithMoyer commented 1 year ago

I support pursuing this POC under the umbrella of this SIG.

I also want to echo Usama's note on the value of formal verification; if there is any novel protocol usage, forming a model of it should be included in the scope of the effort.

gkostal commented 1 year ago

+1 to Keith's statements. I too support pursuing this POC, along with a formal verification, under the umbrella of this SIG.

muhammad-usama-sardar commented 1 year ago

I also want to echo Usama's note on the value of formal verification; if there is any novel protocol usage, forming a model of it should be included in the scope of the effort.

Can you explain what exactly you mean by novel protocol usage? If the protocol has no usage, why design it and why should SIG go for its implementation in the first place? It doesn't make sense to me that you support the implementation of protocol unconditionally, but verification only with a condition. So I would like to better understand your if condition. Unless SIG wants to design a broken protocol, I would argue its verification is a must.

yogeshbdeshpande commented 1 year ago

+1 for formal verification in addition to the POC under the umbrella of Attestation SIG

thomas-fossati commented 1 year ago

@KeithMoyer @MikeCamel @gkostal @shnwc: I'd like to create a repo for this project under the CCC-Attestation org, say CCC-Attestation/attested-tls-poc for hosting related documentation and code -- and also to be able to have an issue tracker and one or more boards. Are you OK with that?

gkostal commented 1 year ago

@KeithMoyer @MikeCamel @gkostal @shnwc: I'd like to create a repo for this project under the CCC-Attestation org, say CCC-Attestation/attested-tls-poc for hosting related documentation and code -- and also to be able to have an issue tracker and one or more boards. Are you OK with that?

I am OK with that.

thomas-fossati commented 1 year ago

Thanks Greg!

Hearing no push back from the other chairs I'll go ahead and create the repo then.

KeithMoyer commented 1 year ago

If the protocol has no usage, why design it and why should SIG go for its implementation in the first place?

@muhammad-usama-sardar My if condition was meant to highlight the "novel" aspect of the statement, not the "usage" aspect. If this POC's protocol is at all novel, it should be modeled to gain confidence in its claimed properties. I do believe it to be novel, so I expect modeling to be done; I was only leaving open the possibility for the project to claim that nothing is novel over existing models (and that claim would need to be scrutinized).

thomas-fossati commented 1 year ago

This has now been accepted and it's currently worked on in https://github.com/CCC-Attestation/attested-tls-poc