commit 7a369f34e10b2890dfca4a0c7ba95e0985c94ccb Author: Tobias Eidelpes Date: Mon May 10 10:46:43 2021 +0200 Initial commit diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..92e4952 --- /dev/null +++ b/.gitignore @@ -0,0 +1,8 @@ +*.zip + +*.aux +*.fdb_latexmk +*.fls +*.log +*.out +*.synctex.gz diff --git a/ca-signed-auth.pv b/ca-signed-auth.pv new file mode 100644 index 0000000..fd7b73e --- /dev/null +++ b/ca-signed-auth.pv @@ -0,0 +1,65 @@ +(* Honest participants *) +free C,S. + +(* Channel *) +free c. + +free hello,ack. + +(* Shared secret between C and S *) +private free m. +(* Secret signing key of CA *) +private free dkCA. + +fun vk/1. +fun ek/1. +fun h/1. + +fun sign/2. +reduc checksign(sign(m,k),vk(k)) = m. +reduc getmess(sign(m,k)) = m. + +fun aenc/2. +reduc adec(aenc(m,ek(k)),k) = m. + +fun senc/2. +reduc sdec(senc(m,k),k) = m. + +query ev:endServerAuth(x,y) ==> ev:beginServerAuth(x,y). +query ev:endClientAuth(x,y,z) ==> ev:beginClientAuth(x,y,z). + +let client = + in(d,(idC,idS)); + new nC; + out(c,(hello,nC)); + in(c,(=hello,nS)); + in(c,(cert,=vk(dkCA))); + let (=idS,ekS)=checksign(cert,vk(dkCA)) in + new secret; + out(c,aenc(secret,ekS)); + event beginClientAuth(nC,nS,secret); + let k=h((secret,nC,nS)) in + out(c,senc((m),k)); + in(c,x); + let (=ack)=sdec(x,k) in + event endServerAuth(nC,nS). + +let server = + in(d,(idC,idS)); + new dkS; + in(c,(=hello,nC)); + new nS; + event beginServerAuth(nC,nS); + out(c,(hello,nS)); + out(c,(sign((idS,ek(dkS)),dkCA),vk(dkCA))); + in(c,x); + let secret=adec(x,dkS) in + let k=h((secret,nC,nS)) in + in(c,y); + let (=m)=sdec(y,k) in + event endClientAuth(nC,nS,secret); + out(c,senc((ack),k)). + +process + new d; + ! (out(d,(C,S)) | client | server) diff --git a/commit1.pv b/commit1.pv new file mode 100644 index 0000000..6556769 --- /dev/null +++ b/commit1.pv @@ -0,0 +1,26 @@ +(* Channel *) +free d. + +(* secret message *) +private free m. + +fun commit/2. +fun open/3. + +equation open(commit(m,k),m,k) = m. + +query attacker:m phase 1. + +noninterf m. + +let alice = + phase 1; + new k; + out(d,commit(m,k)). + +let server = + phase 1; + in(d,x). + +process + alice | server diff --git a/commit2.pv b/commit2.pv new file mode 100644 index 0000000..8cda387 --- /dev/null +++ b/commit2.pv @@ -0,0 +1,31 @@ +(* Channel *) +free d. + +(* secret message *) +private free m. + +fun commit/2. +fun open/3. + +equation open(commit(m,k),m,k) = m. + +query attacker:m phase 1. + +noninterf m. + +let alice = + phase 1; + new k; + out(d,commit(m,k)); + phase 2; + out(d,(m,k)). + +let server = + phase 1; + in(d,x); + phase 2; + in(d,(m,k)); + let (=m)=(open(x,m,k)) in 0. + +process + alice | server diff --git a/passport-trace/trace1.dot b/passport-trace/trace1.dot new file mode 100644 index 0000000..4f3af54 --- /dev/null +++ b/passport-trace/trace1.dot @@ -0,0 +1,245 @@ +digraph { +graph [ordering = out] +edge [arrowhead = none, penwidth = 1.6, fontsize = 30] +node [shape = point, width = 0, height = 0, fontsize = 30] +Trace [label = +>, shape = plaintext] +P0__0 [label = "Honest Process", shape = plaintext] +P__0 [label = "Attacker", shape = plaintext] +Trace -> P0__0 [label = "", style = invisible, weight = 100]{rank = same; P0__0 P__0} +P0__0 -> P0__1 [label = <>, weight = 100] +P0__1 -> P0__2 [label = <>, weight = 100] +P0__2 [shape = plaintext, label = <
{1}new ke1_1
{2}new km1_1
{3}new ke2_1
{4}new km2_1
{5}new d_1
>] +P0__2 -> P0__3 [label = <>, weight = 100] +/*RPar */ +P0__3 -> P0_5__3 [label = <>] +P0__3 -> P0_4__3 [label = <>] +P0__3 -> P0_3__3 [label = <>] +P0__3 -> P0_2__3 [label = <>] +P0__3 -> P0_1__3 [label = <>] +P0__3 -> P0_0__3 [label = <>] +P0__3 [label = "", fixedsize = false, width = 0, height = 0, shape = none] +{rank = same; P0_0__3 P0_1__3 P0_2__3 P0_3__3 P0_4__3 P0_5__3} +P0_1__3 -> P0_1__4 [label = <>, weight = 100] +P0_1__4 [shape = plaintext, label = <
Beginning of process passport
>] +P0_1__4 -> P0_1__5 [label = <>, weight = 100] +P0_2__3 -> P0_2__4 [label = <>, weight = 100] +P0_2__4 [shape = plaintext, label = <
Beginning of process passport
>] +P0_2__4 -> P0_2__5 [label = <>, weight = 100] +P0_5__3 [label = "!", shape = ellipse] +P0_5_0__3 [label = "", fixedsize = false, width = 0, height = 0, shape = none] +P0_5__3 -> P0_5_0__3 [label = <>, weight = 100] +P0_5_0__3 -> P0_5_0__4 [label = <>, weight = 100] +P0_5_0__4 [shape = plaintext, label = <
Beginning of process reader
>] +P0_5_0__4 -> P0_5_0__5 [label = <>, weight = 100] +P0_5_0__5 -> P0_5_0__6 [label = <>, weight = 100] +P0_4__3 -> P0_4__4 [label = <>, weight = 100] +{rank = same; P0_4__4 P0_5_0__6} +P0_5_0__6 -> P0_5_0__7 [label = <>, weight = 100] +P0_4__4 -> P0_4__5 [label = <>, weight = 100] +{rank = same; P0_4__5 P0_5_0__7} +P0_5_0__7 -> P0_4__5 [label = <(ke1_1,km1_1)>, dir = back, arrowhead = normal] +P0_5_0__7 -> P0_5_0__8 [label = <>, weight = 100] +P0_4__5 -> P0_4__6 [label = <>, weight = 100] +{rank = same; P0_4__6 P0_5_0__8} +P0_4__7 [label = "", width = 0.3, height = 0.3] +P0_4__6 -> P0_4__7 [label = <>, weight = 100] +P0_5_0__8 -> P0_5_0__9 [label = <>, weight = 100] +P0_4__8 [label = "", style = invisible] +P0_4__7 -> P0_4__8 [label = <>, weight = 100, style = invisible] +P0_3__3 -> P0_3__4 [label = <>, weight = 100] +P0_2__5 -> P0_2__6 [label = <>, weight = 100] +P0_1__5 -> P0_1__6 [label = <>, weight = 100] +P0_0__3 -> P0_0__4 [label = <>, weight = 100] +P__0 -> P__1 [label = <>, weight = 100] +{rank = same; P__1 P0_0__4 P0_1__6 P0_2__6 P0_3__4 P0_4__8 P0_5_0__9} +P0_5_0__9 -> P0_5_0__10 [label = <>, weight = 100] +P__1 -> P__2 [label = <>, weight = 100] +{rank = same; P__2 P0_5_0__10} +P0_5_0__10 -> P__2 [label = <~M = GetC>, arrowhead = normal] +P0_5_0__10 -> P0_5_0__11 [label = <>, weight = 100] +P0_4__9 [label = "", style = invisible] +P0_4__8 -> P0_4__9 [label = <>, weight = 100, style = invisible] +P0_3__4 -> P0_3__5 [label = <>, weight = 100] +P0_2__6 -> P0_2__7 [label = <>, weight = 100] +P0_1__6 -> P0_1__7 [label = <>, weight = 100] +P0_0__4 -> P0_0__5 [label = <>, weight = 100] +P__2 -> P__3 [label = <>, weight = 100] +{rank = same; P__3 P0_0__5 P0_1__7 P0_2__7 P0_3__5 P0_4__9 P0_5_0__11} +P0_5_0__11 -> P0_5_0__12 [label = <>, weight = 100] +P0_4__10 [label = "", style = invisible] +P0_4__9 -> P0_4__10 [label = <>, weight = 100, style = invisible] +P0_3__5 -> P0_3__6 [label = <>, weight = 100] +P0_2__7 -> P0_2__8 [label = <>, weight = 100] +P0_1__7 -> P0_1__8 [label = <>, weight = 100] +P0_0__5 -> P0_0__6 [label = <>, weight = 100] +P__3 -> P__4 [label = <>, weight = 100] +{rank = same; P__4 P0_0__6 P0_1__8 P0_2__8 P0_3__6 P0_4__10 P0_5_0__12} +P0_5_0__12 -> P0_5_0__13 [label = <>, weight = 100] +P__4 -> P__5 [label = <>, weight = 100] +{rank = same; P__5 P0_5_0__13} +P0_5_0__13 -> P__5 [label = , dir = back, arrowhead = normal] +P0_5_0__13 -> P0_5_0__14 [label = <>, weight = 100] +P0_4__11 [label = "", style = invisible] +P0_4__10 -> P0_4__11 [label = <>, weight = 100, style = invisible] +P0_3__6 -> P0_3__7 [label = <>, weight = 100] +P0_2__8 -> P0_2__9 [label = <>, weight = 100] +P0_1__8 -> P0_1__9 [label = <>, weight = 100] +P0_0__6 -> P0_0__7 [label = <>, weight = 100] +P__5 -> P__6 [label = <>, weight = 100] +{rank = same; P__6 P0_0__7 P0_1__9 P0_2__9 P0_3__7 P0_4__11 P0_5_0__14} +P0_5_0__14 -> P0_5_0__15 [label = <>, weight = 100] +P0_5_0__15 [shape = plaintext, label = <
{10}new nr_4
{11}new kr_4
>] +P0_5_0__15 -> P0_5_0__16 [label = <>, weight = 100] +P0_5_0__16 -> P0_5_0__17 [label = <>, weight = 100] +P0_4__12 [label = "", style = invisible] +P0_4__11 -> P0_4__12 [label = <>, weight = 100, style = invisible] +P0_3__7 -> P0_3__8 [label = <>, weight = 100] +P0_2__9 -> P0_2__10 [label = <>, weight = 100] +P0_1__9 -> P0_1__10 [label = <>, weight = 100] +P0_0__7 -> P0_0__8 [label = <>, weight = 100] +P__6 -> P__7 [label = <>, weight = 100] +{rank = same; P__7 P0_0__8 P0_1__10 P0_2__10 P0_3__8 P0_4__12 P0_5_0__17} +P0_5_0__17 -> P0_5_0__18 [label = <>, weight = 100] +P__7 -> P__8 [label = <>, weight = 100] +{rank = same; P__8 P0_5_0__18} +P0_5_0__18 -> P__8 [label = <~M_1 = sign(senc((nr_4,a_1,kr_4),ke1_1),km1_1)>, arrowhead = normal] +P0_5_0__18 -> P0_5_0__19 [label = <>, weight = 100] +P0_4__13 [label = "", style = invisible] +P0_4__12 -> P0_4__13 [label = <>, weight = 100, style = invisible] +P0_3__8 -> P0_3__9 [label = <>, weight = 100] +P0_2__10 -> P0_2__11 [label = <>, weight = 100] +P0_1__10 -> P0_1__11 [label = <>, weight = 100] +P0_0__8 -> P0_0__9 [label = <>, weight = 100] +P__8 -> P__9 [label = <>, weight = 100] +{rank = same; P__9 P0_0__9 P0_1__11 P0_2__11 P0_3__9 P0_4__13 P0_5_0__19} +P0_5_0__19 -> P0_5_0__20 [label = <>, weight = 100] +P0_4__14 [label = "", style = invisible] +P0_4__13 -> P0_4__14 [label = <>, weight = 100, style = invisible] +P0_3__9 -> P0_3__10 [label = <>, weight = 100] +P0_2__11 -> P0_2__12 [label = <>, weight = 100] +P0_1__11 -> P0_1__12 [label = <>, weight = 100] +P0_0__9 -> P0_0__10 [label = <>, weight = 100] +P__9 -> P__10 [label = <>, weight = 100] +{rank = same; P__10 P0_0__10 P0_1__12 P0_2__12 P0_3__10 P0_4__14 P0_5_0__20} +P0_5_0__20 -> P0_5_0__21 [label = <>, weight = 100] +P__10 -> P__11 [label = <>, weight = 100] +{rank = same; P__11 P0_5_0__21} +P0_5_0__21 -> P__11 [label = , style = dotted] +P0_5_0__21 -> P0_5_0__22 [label = <>, weight = 100] +P0_4__15 [label = "", style = invisible] +P0_4__14 -> P0_4__15 [label = <>, weight = 100, style = invisible] +P0_3__10 -> P0_3__11 [label = <>, weight = 100] +P0_2__12 -> P0_2__13 [label = <>, weight = 100] +P0_1__12 -> P0_1__13 [label = <>, weight = 100] +P0_0__10 -> P0_0__11 [label = <>, weight = 100] +P__11 -> P__12 [label = <>, weight = 100] +{rank = same; P__12 P0_0__11 P0_1__13 P0_2__13 P0_3__11 P0_4__15 P0_5_0__22} +/*RPar */ +P0_5_0__22 -> P0_5_0_1__22 [label = <>] +P0_5_0__22 -> P0_5_0_0__22 [label = <>] +P0_5_0__22 [label = "", fixedsize = false, width = 0, height = 0, shape = none] +{rank = same; P0_5_0_0__22 P0_5_0_1__22} +P0_5_0_1__22 -> P0_5_0_1__23 [label = <>, weight = 100] +P0_5_0_1__23 [shape = plaintext, label = <
Beginning of process passport
>] +P0_5_0_1__23 -> P0_5_0_1__24 [label = <>, weight = 100] +P0_5_0_1__24 -> P0_5_0_1__25 [label = <>, weight = 100] +P0_5_0_0__22 -> P0_5_0_0__23 [label = <>, weight = 100] +{rank = same; P0_5_0_0__23 P0_5_0_1__25} +P0_5_0_1__25 -> P0_5_0_1__26 [label = <>, weight = 100] +P0_5_0_0__23 -> P0_5_0_0__24 [label = <>, weight = 100] +{rank = same; P0_5_0_0__24 P0_5_0_1__26} +P0_5_0_1__26 -> P0_5_0_0__24 [label = <choice[(ke1_1,km1_1),(ke2_1,km2_1)]>, dir = back, arrowhead = normal] +P0_5_0_1__26 -> P0_5_0_1__27 [label = <>, weight = 100] +P0_5_0_0__24 -> P0_5_0_0__25 [label = <>, weight = 100] +{rank = same; P0_5_0_0__25 P0_5_0_1__27} +P0_5_0_0__26 [label = "", width = 0.3, height = 0.3] +P0_5_0_0__25 -> P0_5_0_0__26 [label = <>, weight = 100] +P0_5_0_1__27 -> P0_5_0_1__28 [label = <>, weight = 100] +P0_5_0_0__27 [label = "", style = invisible] +P0_5_0_0__26 -> P0_5_0_0__27 [label = <>, weight = 100, style = invisible] +P0_4__16 [label = "", style = invisible] +P0_4__15 -> P0_4__16 [label = <>, weight = 100, style = invisible] +P0_3__11 -> P0_3__12 [label = <>, weight = 100] +P0_2__13 -> P0_2__14 [label = <>, weight = 100] +P0_1__13 -> P0_1__14 [label = <>, weight = 100] +P0_0__11 -> P0_0__12 [label = <>, weight = 100] +P__12 -> P__13 [label = <>, weight = 100] +{rank = same; P__13 P0_0__12 P0_1__14 P0_2__14 P0_3__12 P0_4__16 P0_5_0_0__27 P0_5_0_1__28} +P0_5_0_1__28 -> P0_5_0_1__29 [label = <>, weight = 100] +P__13 -> P__14 [label = <>, weight = 100] +{rank = same; P__14 P0_5_0_1__29} +P0_5_0_1__29 -> P__14 [label = , dir = back, arrowhead = normal] +P0_5_0_1__29 -> P0_5_0_1__30 [label = <>, weight = 100] +P0_5_0_0__28 [label = "", style = invisible] +P0_5_0_0__27 -> P0_5_0_0__28 [label = <>, weight = 100, style = invisible] +P0_4__17 [label = "", style = invisible] +P0_4__16 -> P0_4__17 [label = <>, weight = 100, style = invisible] +P0_3__12 -> P0_3__13 [label = <>, weight = 100] +P0_2__14 -> P0_2__15 [label = <>, weight = 100] +P0_1__14 -> P0_1__15 [label = <>, weight = 100] +P0_0__12 -> P0_0__13 [label = <>, weight = 100] +P__14 -> P__15 [label = <>, weight = 100] +{rank = same; P__15 P0_0__13 P0_1__15 P0_2__15 P0_3__13 P0_4__17 P0_5_0_0__28 P0_5_0_1__30} +P0_5_0_1__30 -> P0_5_0_1__31 [label = <>, weight = 100] +P0_5_0_1__31 [shape = plaintext, label = <
{43}new nt_4
>] +P0_5_0_1__31 -> P0_5_0_1__32 [label = <>, weight = 100] +P0_5_0_1__32 -> P0_5_0_1__33 [label = <>, weight = 100] +P0_5_0_0__29 [label = "", style = invisible] +P0_5_0_0__28 -> P0_5_0_0__29 [label = <>, weight = 100, style = invisible] +P0_4__18 [label = "", style = invisible] +P0_4__17 -> P0_4__18 [label = <>, weight = 100, style = invisible] +P0_3__13 -> P0_3__14 [label = <>, weight = 100] +P0_2__15 -> P0_2__16 [label = <>, weight = 100] +P0_1__15 -> P0_1__16 [label = <>, weight = 100] +P0_0__13 -> P0_0__14 [label = <>, weight = 100] +P__15 -> P__16 [label = <>, weight = 100] +{rank = same; P__16 P0_0__14 P0_1__16 P0_2__16 P0_3__14 P0_4__18 P0_5_0_0__29 P0_5_0_1__33} +P0_5_0_1__33 -> P0_5_0_1__34 [label = <>, weight = 100] +P__16 -> P__17 [label = <>, weight = 100] +{rank = same; P__17 P0_5_0_1__34} +P0_5_0_1__34 -> P__17 [label = <~M_2 = nt_4>, arrowhead = normal] +P0_5_0_1__34 -> P0_5_0_1__35 [label = <>, weight = 100] +P0_5_0_0__30 [label = "", style = invisible] +P0_5_0_0__29 -> P0_5_0_0__30 [label = <>, weight = 100, style = invisible] +P0_4__19 [label = "", style = invisible] +P0_4__18 -> P0_4__19 [label = <>, weight = 100, style = invisible] +P0_3__14 -> P0_3__15 [label = <>, weight = 100] +P0_2__16 -> P0_2__17 [label = <>, weight = 100] +P0_1__16 -> P0_1__17 [label = <>, weight = 100] +P0_0__14 -> P0_0__15 [label = <>, weight = 100] +P__17 -> P__18 [label = <>, weight = 100] +{rank = same; P__18 P0_0__15 P0_1__17 P0_2__17 P0_3__15 P0_4__19 P0_5_0_0__30 P0_5_0_1__35} +P0_5_0_1__35 -> P0_5_0_1__36 [label = <>, weight = 100] +P0_5_0_0__31 [label = "", style = invisible] +P0_5_0_0__30 -> P0_5_0_0__31 [label = <>, weight = 100, style = invisible] +P0_4__20 [label = "", style = invisible] +P0_4__19 -> P0_4__20 [label = <>, weight = 100, style = invisible] +P0_3__15 -> P0_3__16 [label = <>, weight = 100] +P0_2__17 -> P0_2__18 [label = <>, weight = 100] +P0_1__17 -> P0_1__18 [label = <>, weight = 100] +P0_0__15 -> P0_0__16 [label = <>, weight = 100] +P__18 -> P__19 [label = <>, weight = 100] +{rank = same; P__19 P0_0__16 P0_1__18 P0_2__18 P0_3__16 P0_4__20 P0_5_0_0__31 P0_5_0_1__36} +P0_5_0_1__36 -> P0_5_0_1__37 [label = <>, weight = 100] +P__19 -> P__20 [label = <>, weight = 100] +{rank = same; P__20 P0_5_0_1__37} +P0_5_0_1__37 -> P__20 [label = <~M_1 = sign(senc((nr_4,a_1,kr_4),ke1_1),km1_1)>, dir = back, arrowhead = normal] +P0_5_0_1__37 -> P0_5_0_1__38 [label = <>, weight = 100] +P0_5_0_0__32 [label = "", style = invisible] +P0_5_0_0__31 -> P0_5_0_0__32 [label = <>, weight = 100, style = invisible] +P0_4__21 [label = "", style = invisible] +P0_4__20 -> P0_4__21 [label = <>, weight = 100, style = invisible] +P0_3__16 -> P0_3__17 [label = <>, weight = 100] +P0_2__18 -> P0_2__19 [label = <>, weight = 100] +P0_1__18 -> P0_1__19 [label = <>, weight = 100] +P0_0__16 -> P0_0__17 [label = <>, weight = 100] +P__20 -> P__21 [label = <>, weight = 100] +{rank = same; P__21 P0_0__17 P0_1__19 P0_2__19 P0_3__17 P0_4__21 P0_5_0_0__32 P0_5_0_1__38} +P0_5_0_1__38 -> P0_5_0_1__39 [label = <>, weight = 100] +P0_5_0_1__39 [color = red, shape = plaintext, label = <
{46}let x_3 = checksign(sign(senc((nr_4,a_1,kr_4),
+ke1_1),km1_1),vk(choice[km1_1,km2_1]))
+This process performs a test that may succeed on
+one side and not on the other.
>] +P0_5_0_1__39 -> P0_5_0_1__40 [label = <>, weight = 100] +} \ No newline at end of file diff --git a/passport-trace/trace1.pdf b/passport-trace/trace1.pdf new file mode 100644 index 0000000..7d3f25c Binary files /dev/null and b/passport-trace/trace1.pdf differ diff --git a/passport.pv b/passport.pv new file mode 100644 index 0000000..d108913 --- /dev/null +++ b/passport.pv @@ -0,0 +1,63 @@ +(* Channel *) +free c. + +free error1,error2,GetC. + +fun vk/1. +fun sign/2. +reduc checksign(sign(m,k),vk(k))=m. +reduc getmess(sign(m,k))=m. + +fun senc/2. +reduc sdec(senc(m,k),k)=m. + +let passport = + in(d,(ke,km)); + in(c,=GetC); + new nt; + out(c,nt); + in(c,cert); + let x=checksign(cert,vk(km)) in + let (nr,=nt,kr)=sdec(x,ke) in + new kt; + out(c,sign(senc((nt,nr,kt),ke),km)) + else + out(c,error2) + else + out(c,error1); + 0. + + +let reader = + in(d,(ke,km)); + out(c,GetC); + in(c,nt); + new nr; + new kr; + out(c,sign(senc((nr,nt,kr),ke),km)); + in(c,cert); + let x=checksign(cert,vk(km)) in + let (=nt,=nr,kt)=sdec(x,ke) in + 0. + + +process + new ke1; + new km1; + new ke2; + new km2; + new d; + ( + ! reader (* Start the reader *) + | out(d,(ke1,km1)) (* Send out first key pair *) + | out(d,(ke2,km2)) (* Send out second key pair *) + | passport (* Start first passport *) + | passport (* Start second passport *) + (* Attacker records the signatures sent by reader *) + | phase 1; + ( + (* Start process again with either first or second key pair *) + passport + | out(d,choice[(ke1,km1),(ke2,km2)]) + ) + ) diff --git a/passport_MOD.pv b/passport_MOD.pv new file mode 100644 index 0000000..d7919f6 --- /dev/null +++ b/passport_MOD.pv @@ -0,0 +1,74 @@ +(* Channel *) +free c. + +free error1,GetC. + +fun vk/1. +fun sign/2. +fun true/0. +fun false/0. + +reduc checksign(sign(m,k),vk(k))=m. +reduc getmess(sign(m,k))=m. + +reduc verify(sign(m,k),vk(k))=true + otherwise verify(sign(m,k),x)=false. + +reduc eq(x,x)=true + otherwise eq(x,y)=false. + +reduc and(true,true)=true + otherwise and(x,y)=false. + +fun senc/2. +reduc sdec(senc(m,k),k)=m. + +let passport = + in(d,(ke,km)); + in(c,=GetC); + new nt; + out(c,nt); + in(c,cert); + let x=getmess(cert) in + let (nr,nt2,kr)=sdec(y,ke) in + if and(verify(cert,vk(km)),eq(nt,nt2))=false then + out(c,error1) + else + new kt; + out(c,sign(senc((nt,nr,kt),ke),km)); + 0. + + +let reader = + in(d,(ke,km)); + out(c,GetC); + in(c,nt); + new nr; + new kr; + out(c,sign(senc((nr,nt,kr),ke),km)); + in(c,cert); + let x=checksign(cert,vk(km)) in + let (=nt,=nr,kt)=sdec(x,ke) in + 0. + + +process + new ke1; + new km1; + new ke2; + new km2; + new d; + ( + ! reader (* Start the reader *) + | out(d,(ke1,km1)) (* Send out first key pair *) + | out(d,(ke2,km2)) (* Send out second key pair *) + | passport (* Start first passport *) + | passport (* Start second passport *) + (* Attacker records the signatures sent by reader *) + | phase 1; + ( + (* Start process again with either first or second key pair *) + passport + | out(d,choice[(ke1,km1),(ke2,km2)]) + ) + ) diff --git a/proverif.pdf b/proverif.pdf new file mode 100644 index 0000000..6388d62 Binary files /dev/null and b/proverif.pdf differ diff --git a/report/report.pdf b/report/report.pdf new file mode 100644 index 0000000..bc009ca Binary files /dev/null and b/report/report.pdf differ diff --git a/report/report.tex b/report/report.tex new file mode 100644 index 0000000..dab617e --- /dev/null +++ b/report/report.tex @@ -0,0 +1,160 @@ +\documentclass[12pt,a4paper]{article} + +\usepackage[cm]{fullpage} +\usepackage{hyperref} +\usepackage{amsthm} +\usepackage{amsmath} +\usepackage{amsfonts} +\usepackage{amssymb} +\usepackage{xspace} +\usepackage[english]{babel} +\usepackage{fancyhdr} +\usepackage{titling} +\usepackage{graphicx} +\renewcommand{\thesection}{Exercise \projnumber.\arabic{section}:} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% This part needs customization from you % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +% please enter your group number your names and matriculation numbers here +\newcommand{\groupnumber}{5} +\newcommand{\name}{Tobias Eidelpes} +\newcommand{\matriculation}{01527193} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% End of customization % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\newcommand{\projnumber}{1} +\newcommand{\Title}{ProVerif} +\setlength{\headheight}{15.2pt} +\setlength{\headsep}{20pt} +\setlength{\textheight}{680pt} +\pagestyle{fancy} +\fancyhf{} +\fancyhead[L]{Formal Methods for Security and Privacy \projnumber\ - ProVerif} +\fancyhead[C]{} +\fancyhead[R]{Group \groupnumber} +\renewcommand{\headrulewidth}{0.4pt} +\fancyfoot[C]{\thepage} + + +\begin{document} +\thispagestyle{empty} +\noindent\framebox[\linewidth]{% + \begin{minipage}{\linewidth}% + \hspace*{5pt} \textbf{Formal Methods for Security and Privacy (SS2021)} \hfill Prof.~Matteo Maffei \hspace*{5pt}\\ + + \begin{center} + {\bf\Large Project \projnumber~-- \Title} + \end{center} + + \vspace*{5pt}\hspace*{5pt} \hfill TU Wien \hspace*{5pt} +\end{minipage}% +} +\vspace{0.5cm} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + + +\section*{Group \groupnumber} +Our group consists of the following members: +\begin{center} +\textbf{\name} %please fill the information above + +\matriculation %please fill the information above +\end{center} + +\section{Warm Up} + +\paragraph{Results for protocol (a):} + Non-injective agreement is not fulfilled because the attacker can act as a + man-in-the-middle. He first sniffs the initial \texttt{hello} message and + the nonce and forwards it to the responder. The responder sends the hash of + the nonce and the secret key. The identifier contained in the response is + now modified by the attacker to be his own. Since non-injective agreement is + not satisfied, injective agreement is also not satisfied. + + By adding the id of the initiator into the hash of the response, the + attacker cannot pose as the responder, because the initiator would detect + the mismatch. +\paragraph{Results for protocol (b):} + Non-injective and injective agreement hold. + +\section{Self-Signed Certificates} + +\paragraph{Attack 1:} + The attacker can again pose as the server S and exchange nonces with the + client. Then he sends the signed encryption key to the client. The attacker + can decrypt the received secret from the client because the client is using + the encryption key sent by the attacker. Since the attacker now knows all + three parameters to calculate the symmetric key \texttt{k}, it can decrypt + the shared secret \texttt{m}. The attacker also poses as the client and + communicates with the server. Since the attacker knows \texttt{m}, it can + relay all messages exchanged by the two honest participants without either + of them knowing that they are communicating with the attacker. + +\paragraph{Attack 1:} + The second attack works similarly but does not include the honest server as + a participant at all. The attacker simply poses as the server from the + beginning and the honest client will think he is communicating with the + honest server when in fact he is not. + +\paragraph{Why does introducing a certification authority fix the problem?} + By signing the identity of the certificate holder, the attacker cannot pose + as the server anymore. Clients are able to distinguish the certificate from + the attacker from the one signed by the CA, because the attacker's + certificate is not signed by the CA. + + +\section{Commitment Schemes} + +\paragraph{Results for \texttt{commit1.pv}:} + The message \texttt{m} is kept secret (weak secrecy holds). Strong secrecy + holds as well because the attacker does not know the key \texttt{k}. + +\paragraph{Results for \texttt{commit2.pv}:} + The attacker obviously knows the message \texttt{m} after phase 2 because it + is transmitted over a public channel by Alice. Since weak secrecy does not + hold, strong secrecy cannot hold either. + +\paragraph{Results for \texttt{version1.pv}:} + Weak and strong secrecy hold through all phases. + +\paragraph{Results for \texttt{version2.pv}:} + Both $m_1$ and $m_3$ are kept secret. Strong secrecy, however, does not + hold. + +\paragraph{Why is only one version considered secure?} + The second version is not secure because there is only one key $k$ being + used for the three messages. After revealing $m_2$, the attacker gets + information about $m_1$ and $m_3$. + +\section{e-Passports} +\paragraph{Notes on Exercise 1.5:} + Unlinkability is not given by the implementation, because the attacker can + distinguish different passports by their error messages. Two passports are + created at first and they interact with the reader. The attacker can act as + the reader and capture the message. Depending on which error message is + received in subsequent communication, the attacker can infer which of the + two passports it is talking to. If it receives \texttt{error2}, the nonce + check failed and if it receives \texttt{error1}, the signature check failed. + Figure~\ref{fig:passport} provides a trace as generated by ProVerif. + + To fix the protocol to guarantee unlinkability, only one error message is + emitted (\texttt{error1}) instead of two. For this to work, the check is + made whether the signature is correct AND the nonce is correct. If one of + them is not correct, \texttt{error1} is sent. Since there is no second error + message, the attacker is not able to tell different passports apart from + each other. + + \begin{center} + \begin{figure} + \includegraphics[width=1\textwidth]{../passport-trace/trace1.pdf} + \caption{Trace of the attack on the French BAC implementation.} + \label{fig:passport} + \end{figure} + \end{center} + +\end{document} + diff --git a/self-signed-auth.pv b/self-signed-auth.pv new file mode 100644 index 0000000..0c4bb97 --- /dev/null +++ b/self-signed-auth.pv @@ -0,0 +1,58 @@ +free C,S. +free c. + +free hello,ack. + +private free m. + +fun vk/1. +fun ek/1. +fun h/1. + +fun sign/2. +reduc checksign(sign(m,k),vk(k)) = m. + +fun aenc/2. +reduc adec(aenc(m,ek(k)),k) = m. + +fun senc/2. +reduc sdec(senc(m,k),k) = m. + +query ev:endServerAuth(x,y) ==> ev:beginServerAuth(x,y). +query ev:endClientAuth(x,y,z) ==> ev:beginClientAuth(x,y,z). + +let client = + in(d,(idC,idS)); + new nC; + out(c,(hello,nC)); + in(c,(=hello,nS)); + in(c,(cert,vkS)); + let (=vkS,ekS)=checksign(cert,vkS) in + new secret; + out(c,aenc(secret,ekS)); + event beginClientAuth(nC,nS,secret); + let k=h((secret,nC,nS)) in + out(c,senc((m),k)); + in(c,x); + let (=ack)=sdec(x,k) in + event endServerAuth(nC,nS). + +let server = + in(d,(idC,idS)); + new dkS; + in(c,(hello,nC)); + new nS; + event beginServerAuth(nC,nS); + out(c,(hello,nS)); + out(c,(sign((vk(dkS),ek(dkS)),dkS),vk(dkS))); + in(c,x); + let secret=adec(x,dkS) in + let k=h((secret,nC,nS)) in + in(c,y); + let (=m)=sdec(y,k) in + event endClientAuth(nC,nS,secret); + out(c,senc((ack),k)). + +process + new d; + ! (out(d,(C,S)) | client | server) diff --git a/version1.pv b/version1.pv new file mode 100644 index 0000000..e29131f --- /dev/null +++ b/version1.pv @@ -0,0 +1,39 @@ +(* Channel *) +free d. + +fun commit/6. +fun open/3. + +equation open(commit(m1,m2,m3,k1,k2,k3),m1,k1) = m1. +equation open(commit(m1,m2,m3,k1,k2,k3),m2,k2) = m2. +equation open(commit(m1,m2,m3,k1,k2,k3),m3,k3) = m3. + +private free m1,m2,m3. + +query attacker:m1 phase 1. +query attacker:m3 phase 1. + +query attacker:m1 phase 2. +query attacker:m3 phase 2. + +noninterf m1. +noninterf m3. + +let alice = + new k1; + new k2; + new k3; + phase 1; + out(d,commit(m1,m2,m3,k1,k2,k3)); + phase 2; + out(d,(m2,k2)). + +let server = + phase 1; + in(d,x); + phase 2; + in(d,(m2,k2)); + let (=m2)=(open(x,m2,k2)) in 0. + +process + alice | server diff --git a/version2.pv b/version2.pv new file mode 100644 index 0000000..1151fe7 --- /dev/null +++ b/version2.pv @@ -0,0 +1,37 @@ +(* Channel *) +free d. + +fun commit/4. +fun open/3. + +equation open(commit(m1,m2,m3,k),m1,k) = m1. +equation open(commit(m1,m2,m3,k),m2,k) = m2. +equation open(commit(m1,m2,m3,k),m3,k) = m3. + +private free m1,m2,m3. + +query attacker:m1 phase 1. +query attacker:m3 phase 1. + +query attacker:m1 phase 2. +query attacker:m3 phase 2. + +noninterf m1. +noninterf m3. + +let alice = + new k; + phase 1; + out(d,commit(m1,m2,m3,k)); + phase 2; + out(d,(m2,k)). + +let server = + phase 1; + in(d,x); + phase 2; + in(d,(m2,k)); + let (=m2)=(open(x,m2,k)) in 0. + +process + alice | server diff --git a/warmup_a.pv b/warmup_a.pv new file mode 100644 index 0000000..57399c5 --- /dev/null +++ b/warmup_a.pv @@ -0,0 +1,37 @@ +(* Honest participants *) +free C,S. + +(* Channel *) +free c. + +fun h/1. + +free hello, success. + +(* Secret key shared by C and S *) +private free kCS. + +(* Non-injective agreement *) +query ev:end(id1,id2,n) ==> ev:begin(id1,id2,n). + +(* Injective agreement *) +query evinj:end(id1,id2,n) ==> evinj:begin(id1,id2,n). + +let initiator = + in(d,(idI,idR)); + new nonce; + out(c,(hello,nonce)); + in(c,(=idR,=h((nonce,kCS)))); + event end(idR,idI,nonce); + out(c,success). + +let responder = + in(d,(idI,idR)); + in(c,(=hello,nonce)); + event begin(idR,idI,nonce); + out(c,(idR,h((nonce,kCS)))); + in(c,=success). + +process + new d; + ! initiator | ! responder | ! out(d,(S,C)) | ! out(d,(C,S)) diff --git a/warmup_aMOD.pv b/warmup_aMOD.pv new file mode 100644 index 0000000..25a3d71 --- /dev/null +++ b/warmup_aMOD.pv @@ -0,0 +1,37 @@ +(* Honest participants *) +free C,S. + +(* Channel *) +free c. + +fun h/1. + +free hello, success. + +(* Secret key shared by C and S *) +private free kCS. + +(* Non-injective agreement *) +query ev:end(id1,id2,n) ==> ev:begin(id1,id2,n). + +(* Injective agreement *) +query evinj:end(id1,id2,n) ==> evinj:begin(id1,id2,n). + +let initiator = + in(d,(idI,idR)); + new nonce; + out(c,(hello,nonce)); + in(c,(=idR,=h((nonce,kCS,idI)))); + event end(idR,idI,nonce); + out(c,success). + +let responder = + in(d,(idI,idR)); + in(c,(=hello,nonce)); + event begin(idR,idI,nonce); + out(c,(idR,h((nonce,kCS,idI)))); + in(c,=success). + +process + new d; + ! initiator | ! responder | ! out(d,(S,C)) | ! out(d,(C,S)) diff --git a/warmup_b.pv b/warmup_b.pv new file mode 100644 index 0000000..e6b27f5 --- /dev/null +++ b/warmup_b.pv @@ -0,0 +1,67 @@ +(* Honest Hosts (kS = trusted server) *) +free A,B,kS. + +(* Channel for A - B communication *) +free c. +(* Channel for id sharing *) +free d. +(* Channels for cert sharing *) +free e,f. + +(* Private keys of initiator and responder *) +private free kI, kR. + +(* Function for verification key (public), takes private key as param *) +fun vk/1. + +fun sign/2. + +reduc getmess(sign(m,k)) = m. +reduc checksign(sign(m,k),vk(k)) = m. + +free text1,text2,text3. + +query ev:end(id1,id2,nb) ==> ev:begin(id1,id2,nb). +query evinj:end(id1,id2,nb) ==> evinj:begin(id1,id2,nb). + +query ev:end(id2,id1,na) ==> ev:begin(id2,id1,na). +query evinj:end(id2,id1,na) ==> evinj:begin(id2,id1,na). + +let initiator = + in(d,(idI,idR)); + new nb; + out(c,(nb,text1)); + in(c,(certR,x)); (* Receive signed cert from server *) + let (vkR,=idR)=checksign(certR,vk(kS)) in (* Check server sig *) + let (na,=nb,=idI,text2)=checksign(x,vk(kR)) in (* Check responder sig *) + event end(idR,idI,nb); + event begin(idI,idR,na); + in(f,(certI)); + out(c,(certI,sign((nb,na,idR,text3),kI))); + 0. + + +let responder = + in(d,(idI,idR)); + in(c,(nb,text1)); + event begin(idR,idI,nb); + in(e,(certR)); (* Receive signed cert from server *) + new na; + out(c,(certR,sign((na,nb,idI,text2),kR))); + in(c,(certI,x)); + let (vkI,=idI)=checksign(certI,vk(kS)) in (* Check server sig *) + let (=nb,=na,=idR,text3)=checksign(x,vk(kI)) in (* Check initiator sig *) + event end(idI,idR,na); + 0. + +let server = + in(d,(idI,idR)); + new kS; + out(e,sign((vk(kR),idR),kS)); + out(f,sign((vk(kI),idI),kS)); + 0. + +process + new d; + ! out(c,vk(kI)) | ! out(c,vk(kR)) | ! out(c,vk(kS)) | (* Output verification keys *) + ! initiator | ! responder | ! out(d,(A,B)) | ! out(d,(B,A))