[Verifpal] How to model certificates and general message structures
nadim at symbolic.software
Wed Nov 18 17:02:05 CET 2020
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.
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"
> 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!
> Verifpal mailing list
> Verifpal at lists.symbolic.software
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Verifpal