Subject: [pkix] AuthKeyId and CrlEntryExtension.CertificateIssuer

From: "Kemp, David P." <[email-masked]>
Date: Thu, 16 Feb 2012 14:14:02 -0500

That reminds me of a billboard I saw a few years back.  It had only a
picture of a VW Beetle with the caption:

    0-60? Yes.

I'm sure that car conformed with all NHTSA requirements for use on
public roads.  I still wouldn't buy one, because I have additional wants
and needs.

You may choose to read 5280 in any manner you wish.  But we read it in
the manner I described, and choose to purchase/approve/use RP products
that robustly support revocation checking in a manner suitable for
large-scale enterprises.

Dave

Martin Rex wrote:

> The final sentence of section 5 explicitly says this:

>     Conforming applications are not

>     required to support processing of delta CRLs, indirect CRLs, or
CRLs

>     with a scope other than all certificates issued by one CA.

> which means that it is PERFECTLY OK for RPs to not support

> partitioning of CRLs _at_all_.

---

From: Santosh Chokhani <[email-masked]>
Date: Thu, 23 Feb 2012 17:43:21 -0500

Please share your formal specification and proofs for 5280 with us.

We would love to see how you are so confident that you have not made errors in converting 5280 descriptions into a formal specification.

-----Original Message-----
From: Martin Rex [mailto:[email-masked]] 
Sent: Wednesday, February 22, 2012 5:08 PM
To: Santosh Chokhani
Cc: [email-masked]; [email-masked]
Subject: Re: [pkix] AuthKeyId and CrlEntryExtension.CertificateIssuer

Santosh Chokhani wrote:
> 
> Your formal logic in this case is in serious need of debugging.

Debugging is a method to search for defects in trial-and-error approaches to design and implementation.

If you apply formal correctness proofing to specifications, the result is provable ambiguities and contradictions.

Maybe you're just not familiar with reviewing specification under the aspect of formal correctness proofing in order to find out whether some existing wording is a defect of the spec or some interpretation that seems conceivable at the natural language level is actually inconsistent with the specification.

-Martin