Download HLPSL Tutorial - The AVISPA Project

2.3 Example 3 - security goals
K1ab
N1b
26
: symmetric_key,
: text
const alice_bob_k1ab, alice_bob_na, bob_alice_nb: protocol_id
init State := 0
transition
0. State = 0 /\ RCV(start) =|>
State’:= 2 /\ Na’ := new()
/\ SND(A.{Na’}_Kab)
2. State = 2 /\ RCV({Succ(Na).Nb’}_Kab) =|>
State’:= 4 /\ SND({Succ(Nb’)}_Kab)
/\ witness(A,B,bob_alice_nb,Nb’)
4. State = 4 /\ RCV({K1ab’.N1b’}_Kab) =|>
State’:= 6
/\ request(A,B,alice_bob_k1ab,K1ab’)
/\ request(A,B,alice_bob_na,Na)
end role
——————————————————————————————————————————
role bob (A, B
Kab
Succ
SND, RCV
played_by B
def=
:
:
:
:
agent,
symmetric_key,
hash_func,
channel(dy))
local State
: nat,
Nb,Na,N1b : text,
K1ab
: symmetric_key
init State := 1
transition
AVISPA
HLPSL Tutorial