Possible crypto backdoor in RFC-2631 Diffie-Hellman Key Agreement Method

[Georgi Guninski]

On Mon, Sep 07, 2015 at 12:07:14PM +0000, Alfonso De Gregorio wrote:
> >
> > Comments in [0] suggest "formal verification".
> 
> The only hope to have a formal verification that extends also to
> algebraic properties, is to start from formal specifications. A
> top-down approach in stark contrast with the dynamic, agile, and
> pragmatic "ship, then test" paradigm [1] and the "don't worry, be
> crappy" mantra [2], repeated by entrepreneurs innovating the most.
> 
> We need better security trade-offs.
>

Re "formal verification".

I am skidiot at formal verification (FW).

So far my best achievement in FW is
"Axiom free proof of False" in Coq (is it Cock?).

I did this by native code execution via plugins
in Coq (the plugins were part of the "pr00f"),
which in theory can falsify other proofs
depending on the file permissions.

Much letter I learned that the lovely micro$oft
heavily depend on plugins in their Cock "pr00fs" and
accidentally something broke the check of the
"pr00f" for result of significant importance 
(something like "coqchk") due to some fault in the plugin and/or Coq.

The p00f failure was discussed on academic site.

In short, I consider Coq a charlatan tool,
and likely security vulnerability, since a proof
can easily execute native code.

Let me know if you need further references.

btw, doesn't your post contradict another post of yours
here:
https://cpunks.org/pipermail/cypherpunks/2015-September/009032.html

> While I sympathize with your point of view, and while I would welcome
> a full equivalence of implementations, ...