[Verifpal] How to model certificates and general message structures

Nadim Kobeissi nadim at symbolic.software
Wed Nov 18 17:02:05 CET 2020


Dear Friedrich,

This sounds like an overly general conversation and after thinking about it
for a bit, I think it's better to address it on the Discord since it will
require more back-and-forths than substantive emails, I think.

Nadim Kobeissi
Symbolic Software • https://symbolic.software
Sent from office


On Wed, Nov 4, 2020 at 9:18 PM Friedrich Wiemer via Verifpal
<verifpal at lists.symbolic.software> wrote:

> Dear all,
>
> I have some basic questions regarding protocol modeling and would be
> very happy if someone would take the time to help me out :)
>
> First question: if I understand correctly, verifpal does not support
> modeling of certificates. Would the correct / sound way to model these
> be, to just send the public keys as guarded messages?
> Or is there an alternative way, to model such a "pre-sharing" of the
> public part of a key pair? I guess "leak"ing the public key would work,
> but it sounds a bit hacky (and if only b/c of the implied meaning of"
> leak).
> Additionally, I'm not sure if leaving out the certificate checking on
> reciever side, that would be the correct way in practice, is OK to do?
> Is there a better alternative way?
>
> Second question: how closely should one model the message structures in
> a formal model? For example, if the protocol involves fixed strings
> (like "fst message", "snd message", ... prepended to every 1st,2nd,...
> message), should these be included in the model and checked on each
> receiving? From my understanding this would unnecessarily blow up the
> state space to check during verification and thus slow down the whole
> process, while not giving much possibilities to an attacker anyway - is
> that right?
> So would it be a sound approach, to leave out these values?
>
> Thanks a lot in advance!
> Best,
> Friedrich
>
> _______________________________________________
> Verifpal mailing list
> Verifpal at lists.symbolic.software
> https://lists.symbolic.software/mailman/listinfo/verifpal
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20201118/18c96f6b/attachment.htm>


More information about the Verifpal mailing list