Re: [CFRG] Adoption Call: Guidelines for Writing Cryptography Specifications

[Deirdre Connolly <[e-mail]>]

I agree with Chris on these points on formality, formal language, notation,
and security definitions.

These questions also pertain to other questions upthread: if these are to
be as formal as expected in a full paper under submission,
does that imply LaTeX or more-exotic-than-ASCII character support? If yes,
would this formal language be interspersed in
specs amongst algorithm pseudocode? I know for some implementers, such
formal language may be intimidating, vs
a prose/informal description. I know for protocol designers or researchers,
having such formally defined security notions
alongside the spec is valuable, but these recommendations are trying to
serve multiple audiences. In my opinion,
a more informal summary of security properties is sufficient, with links to
full formally defined security notions and/or proofs
that those properties are upheld by the protocol under specification. If
such resources do not exist, I'm not sure the best place
for them: perhaps an appendix, but putting a full proof in the appendix of
an IRTF RFC seems incorrect.

Having specific examples would help clarify these questions, as Chris
mentioned.

On Fri, Jun 9, 2023 at 7:27 PM Christopher Patton <cpatton=
[e-mail]> wrote:

> I whole-heartedly support adoption. I think this would be a useful
> resource. (I particularly like the idea of including a list of exemplary
> specs and specs that didn't quite serve their purpose.)
>
> I think my primary concern is that this draft touches on a few aspects of
> spec writing that are somewhat subjective. In particular the draft uses the
> term "formal" as if all readers have the same bar for what "formality"
> entails. I'm not sure if anything can really be done about this, but there
> may be specific instances where we can provide some concrete
> recommendations.
>
> Specific comments:
>
>    1. Section 3.2 "Precision": It would be useful to cite specific
>    examples where ambiguous specs (including those outside the CFRG) lead to
>    security vulnerabilities.
>    2. Section 3.2 "Precision": "[use] formal notation or pseudocode": To
>    me this feels too subjective. I realize this is the bikeshed of all
>    bikesheds (for our community in particular), but I wonder if it
>    could/should be in scope for a draft like this to come up with a concrete
>    recommendation. It would be wonderful if all or many CFRG drafts used the
>    same language. (I think a similar point can also be made about mathematical
>    notation, though there I feel less strongly: consistency throughout the
>    document, and clear definitions, are sufficient.)
>    3. Section 4.2.2 "Formalizing Security Definitions":  "Specification
>    authors should strive to express security definitions in a formal
>    language": What bar are you trying to get spec authors to cross here? Like,
>    "the ciphertext does not leak the plaintext" is pretty informal; "the
>    ciphertext is computationally indistinguishable from a random string" is
>    more formal; (forall A)(forall poly) Pr[A(C<-$Enc(K,M)) => 1] - Pr[A($) =>
>    1] < poly is even more formal.
>
> Best,
> Chris P.
>
> On Thu, Jun 1, 2023 at 10:14 PM Stanislav V. Smyshlyaev <[e-mail]>
> wrote:
>
>> Dear CFRG participants,
>>
>> This message is starting 3 weeks adoption call on "Guidelines for
>> Writing Cryptography Specifications" draft,
>> draft-sullivan-cryptography-specification-00 (
>> https://datatracker.ietf.org/doc/draft-sullivan-cryptography-specification/)
>> that will end on June 23rd 2023.
>>
>> Please send your feedback in reply to this email or directly to CFRG
>> chairs <[e-mail]> <[e-mail]>.
>>
>> Best regards,
>> Stanislav (for CFRG chairs)
>> _______________________________________________
>> CFRG mailing list
>> [e-mail]
>> https://www.irtf.org/mailman/listinfo/cfrg
>>
> _______________________________________________
> CFRG mailing list
> [e-mail]
> https://www.irtf.org/mailman/listinfo/cfrg
>