Skip to content

Commit 7557821

Browse files
ArquintLArquintL
committed
adapts DH initiator implementation to verify again
1 parent a7ddc5c commit 7557821

File tree

25 files changed

+665
-135
lines changed

25 files changed

+665
-135
lines changed

‎dh/implementation/initiator/initiator.go‎

Lines changed: 15 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,8 @@ import . "dh-gobra/library"
66
//@ import ft "dh-gobra/verification/fact"
77
//@ import pl "dh-gobra/verification/place"
88
//@ import io "dh-gobra/verification/iospec"
9-
//@ import tm "dh-gobra/verification/util"
9+
//@ import tm "dh-gobra/verification/utilterm"
10+
//@ import ay "dh-gobra/verification/utilbytes"
1011
//@ import am "dh-gobra/verification/term"
1112
//@ import p "dh-gobra/verification/pattern"
1213
//@ import pub "dh-gobra/verification/pub"
@@ -27,13 +28,15 @@ pred (i *Initiator) Mem(skAT, skBT tm.Term) {
2728
}
2829
2930
ghost
31+
decreases
3032
requires acc(i.Mem(skAT, skBT), _)
3133
pure
3234
func (i *Initiator) getIdA(skAT, skBT tm.Term) uint32 {
3335
return unfolding acc(i.Mem(skAT, skBT), _) in i.idA
3436
}
3537
3638
ghost
39+
decreases
3740
requires acc(i.Mem(skAT, skBT), _)
3841
pure
3942
func (i *Initiator) getIdB(skAT, skBT tm.Term) uint32 {
@@ -43,14 +46,14 @@ func (i *Initiator) getIdB(skAT, skBT tm.Term) uint32 {
4346

4447
//@ requires l.Mem()
4548
//@ requires pl.token(t) && io.P_Alice(t, am.freshTerm(fresh.fr_integer32(rid)), mset[ft.Fact]{})
46-
//@ requires rid != 0 && rid != 1
49+
//@ requires rid < 0 || 2 < rid
4750
//@ ensures l.Mem()
4851
func RunInitiator(l *LibState, rid uint32 /*@, ghost t pl.Place @*/) (err error) {
4952
//@ ridT := tm.integer32(rid)
5053
//@ s := mset[ft.Fact]{}
5154

5255
//@ unfold io.P_Alice(t, ridT, s)
53-
//@ unfold io.phiRF_Alice_5(t, ridT, s)
56+
//@ unfold io.phiRF_Alice_7(t, ridT, s)
5457
//@ assert acc(io.e_Setup_Alice(t, ridT))
5558
//@ skAT := io.get_e_Setup_Alice_r3(t, ridT)
5659
//@ skBT := io.get_e_Setup_Alice_r4(t, ridT)
@@ -74,7 +77,7 @@ func RunInitiator(l *LibState, rid uint32 /*@, ghost t pl.Place @*/) (err error)
7477

7578
// create x
7679
//@ unfold io.P_Alice(t1, ridT, s1)
77-
//@ unfold io.phiRF_Alice_3(t1, ridT, s1)
80+
//@ unfold io.phiRF_Alice_5(t1, ridT, s1)
7881
//@ assert acc(io.e_FrFact(t1, ridT))
7982
//@ xT := io.get_e_FrFact_r1(t1, ridT)
8083
var x []byte
@@ -170,7 +173,7 @@ func (i *Initiator) sendMsg1(X []byte /*@, ghost skAT tm.Term, ghost skBT tm.Ter
170173
}
171174

172175
//@ unfold io.P_Alice(t1, ridT, s1)
173-
//@ unfold io.phiRG_Alice_2(t1, ridT, s1)
176+
//@ unfold io.phiRG_Alice_4(t1, ridT, s1)
174177
//@ assert io.e_OutFact(t1, ridT, XT)
175178
err /*@, t1 @*/ = i.l.Send(msg1Data /*@, t1, ridT, XT @*/)
176179
//@ s1 = s1 setminus mset[ft.Fact]{ ft.OutFact_Alice(ridT, XT) }
@@ -190,7 +193,7 @@ func (i *Initiator) sendMsg1(X []byte /*@, ghost skAT tm.Term, ghost skBT tm.Ter
190193
func (i *Initiator) recvMsg2(X []byte, /*@ ghost skAT tm.Term, ghost skBT tm.Term, ghost xT tm.Term, ghost t pl.Place, ghost ridT tm.Term, ghost s mset[ft.Fact] @*/) (receivedY []byte, err error /*@, ghost YT tm.Term, ghost t1 pl.Place, ghost s1 mset[ft.Fact] @*/) {
191194
//@ unfold acc(i.Mem(skAT, skBT), 1/2)
192195
//@ unfold io.P_Alice(t, ridT, s)
193-
//@ unfold io.phiRF_Alice_4(t, ridT, s)
196+
//@ unfold io.phiRF_Alice_6(t, ridT, s)
194197
//@ assert io.e_InFact(t, ridT)
195198
var signedMsg2 []byte
196199
//@ ghost var msg2T tm.Term
@@ -232,8 +235,9 @@ func (i *Initiator) recvMsg2(X []byte, /*@ ghost skAT tm.Term, ghost skBT tm.Ter
232235
//@ idBT := tm.integer32(i.getIdB(skAT, skBT))
233236
//@ XT := tm.exp(tm.generator(), xT)
234237
//@ YT := p.patternRequirement2(ridT, idAT, idBT, skAT, skBT, xT, by.oneTerm(Abs(receivedY)), msg2T, t1, s1)
235-
// the following assert stmt is needed for triggering reasons:
236-
//@ assert by.getMsgB(Abs(signedMsg2)) == Abs(msg2Data)
238+
// the following 2 assert stmts are needed for triggering reasons:
239+
//@ assert ay.getMsgB(Abs(signedMsg2)) == Abs(msg2Data)
240+
//@ assert by.ex55B(Abs(msg2Data)) == Abs(receivedY)
237241
//@ assert Abs(receivedY) == by.gamma(YT)
238242

239243
//@ unfold io.P_Alice(t1, ridT, s1)
@@ -246,7 +250,8 @@ func (i *Initiator) recvMsg2(X []byte, /*@ ghost skAT tm.Term, ghost skBT tm.Ter
246250
cl.IN_ALICE(YT, tm.tuple5(tm.integer32(Msg2Tag), idBT, idAT, XT, YT)),
247251
cl.Secret(idAT, idBT, tm.exp(YT, xT)),
248252
cl.Running(tm.idR(), tm.idI(), tm.tuple3(idAT, idBT, tm.exp(YT, xT))),
249-
cl.Commit(tm.idI(), tm.idR(), tm.tuple3(idAT, idBT, tm.exp(YT, xT))) }
253+
cl.Commit(tm.idI(), tm.idR(), tm.tuple3(idAT, idBT, tm.exp(YT, xT))),
254+
cl.AliceHsDone(tm.exp(YT, xT)) }
250255
r := mset[ft.Fact]{ ft.St_Alice_2(ridT, idAT, idBT, skAT, skBT, xT, YT),
251256
ft.OutFact_Alice(ridT, msg3T) }
252257
@*/
@@ -287,7 +292,7 @@ func (i *Initiator) sendMsg3(X, receivedY []byte /*@, ghost skAT tm.Term, ghost
287292
//@ XT := tm.exp(tm.generator(), xT)
288293
//@ msgT := tm.sign(tm.tuple5(tm.integer32(Msg3Tag), idAT, idBT, YT, XT), skAT)
289294
//@ unfold io.P_Alice(t, ridT, s)
290-
//@ unfold io.phiRG_Alice_2(t, ridT, s)
295+
//@ unfold io.phiRG_Alice_4(t, ridT, s)
291296
//@ assert acc(io.e_OutFact(t, ridT, msgT))
292297
err /*@, t1 @*/ = i.l.Send(signedMsg3 /*@, t, ridT, msgT @*/)
293298
//@ s1 = s setminus mset[ft.Fact]{ ft.OutFact_Alice(ridT, msgT) }

‎dh/implementation/library/crypto.go‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,8 @@ import sign "golang.org/x/crypto/nacl/sign"
1111
//@ import . "dh-gobra/verification/place"
1212
//@ import . "dh-gobra/verification/iospec"
1313
//@ import am "dh-gobra/verification/term"
14-
//@ import tm "dh-gobra/verification/util"
14+
//@ import by "dh-gobra/verification/utilbytes"
15+
//@ import tm "dh-gobra/verification/utilterm"
1516

1617
const NonceLength = 24
1718

@@ -97,7 +98,7 @@ func (l *LibState) expMod(base, exp []byte) (res []byte, err error) {
9798
//@ preserves acc(l.Mem(), 1/16)
9899
//@ preserves acc(Mem(exp), 1/16)
99100
//@ ensures err == nil ==> Mem(res)
100-
//@ ensures err == nil ==> Abs(res) == expB(generatorB(), Abs(exp))
101+
//@ ensures err == nil ==> Abs(res) == expB(by.generatorB(), Abs(exp))
101102
// arg is big-endian
102103
func (l *LibState) DhExp(exp []byte) (res []byte, err error) {
103104
g := big.NewInt(GroupGenerator)
@@ -156,6 +157,7 @@ func (l *LibState) Open(signedData []byte, pk []byte /*@, ghost skT tm.Term @*/)
156157
}
157158

158159
//@ trusted
160+
//@ decreases
159161
//@ requires acc(Mem(s1), 1/16) && acc(Mem(s2), 1/16)
160162
//@ ensures res == (Abs(s1) == Abs(s2))
161163
//@ pure

‎dh/implementation/library/io.go‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ import fmt "fmt"
55
//@ import . "dh-gobra/verification/bytes"
66
//@ import . "dh-gobra/verification/place"
77
//@ import . "dh-gobra/verification/iospec"
8-
//@ import tm "dh-gobra/verification/util"
8+
//@ import tm "dh-gobra/verification/utilterm"
99

1010
const MAX_DATA_SIZE = 1024
1111

‎dh/implementation/library/marshal.go‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@ package library
33
import binary "encoding/binary"
44
import errors "errors"
55
//@ import . "dh-gobra/verification/bytes"
6+
//@ import by "dh-gobra/verification/utilbytes"
67

78
const Msg2Tag uint32 = 0
89
const Msg3Tag uint32 = 1
@@ -52,7 +53,7 @@ func (l *LibState) MarshalMsg1(msg1 *Msg1) (res []byte, err error) {
5253
//@ trusted
5354
//@ preserves acc(Mem(data), 1/16)
5455
//@ ensures err == nil ==> res.Mem()
55-
//@ ensures err == nil ==> Abs(data) == (unfolding acc(res.Mem(), 1/16) in tuple5B(integer32B(Msg2Tag), integer32B(res.IdB), integer32B(res.IdA), Abs(res.X), Abs(res.Y)))
56+
//@ ensures err == nil ==> Abs(data) == (unfolding acc(res.Mem(), 1/16) in by.tuple5B(by.integer32B(Msg2Tag), by.integer32B(res.IdB), by.integer32B(res.IdA), Abs(res.X), Abs(res.Y)))
5657
func (l *LibState) UnmarshalMsg2(data []byte) (res *Msg2, err error) {
5758
if len(data) < 2 * DHHalfKeyLength + 12 {
5859
return nil, errors.New("msg2 is too short")
@@ -75,7 +76,7 @@ func (l *LibState) UnmarshalMsg2(data []byte) (res *Msg2, err error) {
7576
//@ trusted
7677
//@ preserves acc(msg3.Mem(), 1/16)
7778
//@ ensures err == nil ==> Mem(res)
78-
//@ ensures err == nil ==> Abs(res) == (unfolding acc(msg3.Mem(), 1/16) in tuple5B(integer32B(Msg3Tag), integer32B(msg3.IdA), integer32B(msg3.IdB), Abs(msg3.Y), Abs(msg3.X)))
79+
//@ ensures err == nil ==> Abs(res) == (unfolding acc(msg3.Mem(), 1/16) in by.tuple5B(by.integer32B(Msg3Tag), by.integer32B(msg3.IdA), by.integer32B(msg3.IdB), Abs(msg3.Y), Abs(msg3.X)))
7980
func (l *LibState) MarshalMsg3(msg3 *Msg3) (res []byte, err error) {
8081
res = make([]byte, 12)
8182
binary.BigEndian.PutUint32(res[:4], Msg3Tag)

‎dh/implementation/library/state.go‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ pred (l *LibState) Mem()
1818
pred Mem(data []byte)
1919
2020
ghost
21+
decreases
2122
requires acc(Mem(b), _)
2223
pure func Abs(b []byte) (res by.Bytes)
2324
@*/

0 commit comments

Comments
 (0)