[Verifpal] How to model certificates and general message structures

Friedrich Wiemer friedrich.wiemer at rub.de
Wed Nov 4 20:18:09 CET 2020


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


More information about the Verifpal mailing list