HLPSL
1 program
Added 2026-03-05T10:00:00Z
Agent: claude-codeModel: claude-sonnet-4-6WebSearch: disabled
Evidence
Report issue
View issues
Aliases: High-Level Protocol Specification Language
Provenance: commit b040857813 · authored 2026-03-05T11:47:23+01:00 · agent claude-code · model claude-sonnet-4-6
Sources mentioning this language
1 source · not in taxonomy (canonical name didn't match any upstream)
Related languages
LLM-contributed programs
Symmetric Key Authentication Protocol
Provenance: commit b040857813 · authored 2026-03-05T11:47:23+01:00 · agent claude-code · model claude-sonnet-4-6 · WebSearch disabled
role alice (A, B: agent,
Kab: symmetric_key,
SND, RCV: channel (dy))
played_by A def=
local State : nat,
Na : text
init State := 0
transition
0. State = 0 /\ RCV(start) =|>
State' := 1 /\ Na' := new()
/\ SND({Na'.A.B}_Kab)
1. State = 1 /\ RCV({Na.Nb'}_Kab) =|>
State' := 2 /\ SND({Nb'}_Kab)
end role
role bob (A, B: agent,
Kab: symmetric_key,
SND, RCV: channel (dy))
played_by B def=
local State : nat,
Nb : text,
Na : text
init State := 0
transition
0. State = 0 /\ RCV({Na'.A.B}_Kab) =|>
State' := 1 /\ Nb' := new() /\ Na' := Na
/\ SND({Na.Nb'}_Kab)
/\ secret(Nb', sec_nb, {A, B})
1. State = 1 /\ RCV({Nb}_Kab) =|>
State' := 2
end role
role session(A, B: agent,
Kab: symmetric_key)
def=
local SA, RA, SB, RB: channel (dy)
composition
alice(A, B, Kab, SA, RA)
/\ bob(A, B, Kab, SB, RB)
end role
role environment() def=
const a, b : agent,
kab, kai : symmetric_key,
sec_nb : protocol_id
intruder_knowledge = {a, b, kai}
composition
session(a, b, kab)
/\ session(a, i, kai)
/\ session(i, b, kai)
end role
goal
secrecy_of sec_nb
end goal
environment()