Does anyone still use BAN or GNY logic in practice?
I don't think they are even used academically anymore, possibly because of soundness problems and limited expressivity. I would not recommend this approach.