'Proving' the correctness of a network encryption system test system

Ian Grigg iang at systemics.com
Sat Dec 4 11:49:05 EST 2004


(I thought this was an interesting problem, and was
waiting for a response...)

> Alice has:
>
> 1. A system which does processing of encrypted network streams.

This means encrypting and decrypting network streams?

> Alice wants the following from Bob:
>
> 2. A test system for the processing system in 1. This system is going to
> be used to decide if the processing system in 1 is working (processing)
> as it should.

If you can inject chosen plaintext into the system in
1, then write another system that does the same thing,
run it with the same information, and spit out some
ciphertext.  Then, inject the plaintext into system 1,
and watch for the ciphertext.

> 3. A test system for the test system in 2. This system is going to be
> used
> to decide if the test system in 2 is working (testing) as it should.

Well.  Either write system 3 that does what system 2
does to system 1....  Or, use system 1 to test system 2?
I'd go for the former myself.

> 4. A specification for the test system in 3. This specification shall
> contain
> explicit and well defined critera for how to decide that the test
> system in 2
> is working (testing) as it should.

All three specs should be the same.

> So the question really is; how does Bob convince Alice that the test
> system in
> 2 works (tests) as it should?

Ah.  OK.  How about this:  swap system 1 with 2 during
live usage and revert 1 into testing mode.

> Alice does not need strict formal
> mathematical
> proofs for the correctness of 2, but neither is she going to be
> satisfied by
> hearing Bob (in his best Snake Oil voice) say: "Trust me, I know what
> I'm
> doing..." Does anyone have any good pointers to information about
> problems like
> these?

One good idea is to specify that the entirity of
the system(s) is open source, and Alice can construct
it.  This doesn't prove anything by itself, but it
raises the bar on any errors or weaknesses, because
once identified, they are much easier to find and
resolve.  Far less potential for childish arguments
like "is so, is not."

iang

---------------------------------------------------------------------
The Cryptography Mailing List
Unsubscribe by sending "unsubscribe cryptography" to majordomo at metzdowd.com



More information about the cryptography mailing list