[Verifpal] How to model certificates and general message structures
friedrich.wiemer at rub.de
Wed Nov 4 20:18:09 CET 2020
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
So would it be a sound approach, to leave out these values?
Thanks a lot in advance!
More information about the Verifpal