dear formal methods folk, is there a convenient tool for modelling agent-knowledge in (cryptographic) protocols that I should know of?
I've been playing around in Prolog a little (see image), but I'm sort of drawing a blank on how I'd properly model this.


I know of tools like TLA+ for modelling protocol interactions between agents, and all I'm adding here is a notion of (derived) knowledge, and I strongly doubt I'm the first to want this.

· · Web · 0 · 0 · 0

wait fuck TLA+ isn't the tool I was thinking of, *handwave* process calculus or something, urgh

the point is, I'm a dumbass, help me find tools that'll tell me in which exact ways I'm being a dumbass in protocol design, kthx

I'm now trying to learn ProVerif from the fine folks at Inria
h/t @spun_off (
it seems to do exactly the kind of knowledge-modelling I want

Sign in to participate in the conversation

Server run by the main developers of the project 🐘 It is not focused on any particular niche interest - everyone is welcome as long as you follow our code of conduct!