Detail

SLMC-K – extension of SLMC for checking security protocol verification

SLMC-K is an extension of the SLMC tool for checking ecurity protocol verification. The modelling language is a variant of the applied pi-calculus of Abadi and Fournet, while specifications are expressed in a dynamic spatial logic extended with an epistemic operator that talks about process knowledge.