diff options
| author | jaseg <git@jaseg.net> | 2018-12-17 13:38:39 +0900 |
|---|---|---|
| committer | jaseg <git@jaseg.net> | 2018-12-17 13:38:39 +0900 |
| commit | 447d084d79cc139d0aaa4433148cc7c310bfaf0d (patch) | |
| tree | 4fce2f3db95c5dd62d4e9342c553b74badb822f4 /src/noise.c | |
| parent | 40e9fb8153a218a243cff749d7d0b4e82d70ae94 (diff) | |
| download | secure-hid-447d084d79cc139d0aaa4433148cc7c310bfaf0d.tar.gz secure-hid-447d084d79cc139d0aaa4433148cc7c310bfaf0d.tar.bz2 secure-hid-447d084d79cc139d0aaa4433148cc7c310bfaf0d.zip | |
First steps to prove cobs decoder
Diffstat (limited to 'src/noise.c')
| -rw-r--r-- | src/noise.c | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/src/noise.c b/src/noise.c index 890b5b5..949a68d 100644 --- a/src/noise.c +++ b/src/noise.c @@ -199,8 +199,6 @@ void uninit_handshake(struct NoiseState *st, enum handshake_state new_state) { requires \separated(&usart2_out, st, buf, st->handshake, &st->handshake_hash); - assigns key_checked_trace; - ensures (st->handshake_state == HANDSHAKE_DONE_KNOWN_HOST) ==> key_checked_trace == 1; ensures (st->handshake_state != HANDSHAKE_IN_PROGRESS) ==> key_match_trace == 1 || (st->failed_handshakes > \old(st->failed_handshakes)); |