free c.
free attackerBB.
free auth3.
private free bb.
free id1.
free id2.
free id3.
fun zero/0.
fun one/0.
fun ped/2.
fun forge1/2.
fun forge2/2.
in phase 1 equation forge1(ped(xv, xr), xr) = xv.
in phase 1 equation forge2(ped(xv, xr), xv) = xr.
in phase 1 equation forge1(xp, forge2(xp, yv)) = yv.
in phase 1 equation forge2(xp, forge1(xp, yr)) = yr.
in phase 1 equation ped(xv, forge2(xp, xv)) = xp.
in phase 1 equation ped(forge1(xp, xr), xr) = xp.
future phase 1 with channel bb.
let V =
new s;
let commit = ped(v, s) in (
out(auth, (id, commit, v, s))).
let V1 =
let id = id1 in (
let auth = auth1 in (
let v = choice[zero, one] in (
V))).
let V2 =
let id = id2 in (
let auth = auth2 in (
let v = choice[one, zero] in (
V))).
let B =
new authBT; (
(in(auth1, (=id1, xped1, xv1, xs1));
if xped1 = ped(xv1, xs1)
then (out(bb, (id1, xped1));
out(attackerBB, (id1, xped1));
out(authBT, (id1, xv1)))) |
(in(auth2, (=id2, xped2, xv2, xs2));
if xped2 = ped(xv2, xs2)
then (out(bb, (id2, xped2));
out(attackerBB, (id2, xped2));
out(authBT, (id2, xv2)))) |
(in(auth3, (=id3, xped3, xv3, xs3));
if xped3 = ped(xv3, xs3)
then (out(bb, (id3, xped3));
out(attackerBB, (id3, xped3));
out(authBT, (id3, xv3)))) |
T).
let T =
in(authBT, (=id1, yv1)); in(authBT, (=id2, yv2)); in(authBT, (=id3, yv3)); (
out(bb, choice[yv1, yv2]) |
out(attackerBB, choice[yv1, yv2]) |
out(bb, choice[yv2, yv1]) |
out(attackerBB, choice[yv2, yv1]) |
out(bb, yv3) |
out(attackerBB, yv3)).
process new skE; new auth1; new auth2; (
V1 | V2 | B)