Re: [irtf-discuss] Usable formal methods side meeting at IETF 115

[Sampo Syreeni <[e-mail]>]

On 2022-11-06, Buday Gergely wrote:

> May I get examples of these overly complex protocols and network 
> environments, and the formalisms that that cannot handle these 
> complexities?

So let's try and find a counter-example. Suppose an early PGP style Web 
of Trust, where every participant can vouch for another participant's 
key. But also at any time can withdraw and recertify their voucher. 
Crucially, if there are two or more people vouching for some signature, 
even by way of rumour, they add up to more reliance on a key.

How precisely do you generalize or verify such a protocol when the 
number of verifying nodes goes to infinity? Especially if you model the 
process of growing the WoT as not random, but adversarial? How precisely 
would you defend your proof software against me making it 
computationally expensive, at each step, to grow my adversarial web of 
trust?

Because I think, in this highly realistic problem, I could build up a 
WoT whose recognizers would bump upto at least the travelling salesman 
problem. Maybe the graph isomorphism one at that. I don't yet know how 
to make the problem downright uncomputable/indecidable, but even that 
might be on the table.

I believe all in here is about finding a properly limited logical 
framework, with some mathematical power. If you go too shallow, you're 
not going to get your problem described. But if you go deep, then your 
machinery is not going to work out either. You'll bump into no-go 
proofs.
-- 
Sampo Syreeni, aka decoy - [e-mail], http://decoy.iki.fi/front
[phone], 025E D175 ABE5 027C 9494 EEB0 E090 8BA9 0509 85C2