Commit 79632748 authored by Kayla Mesh's avatar Kayla Mesh

Minor changes to my spec

parent f86f416c
......@@ -66,7 +66,7 @@ Theory
eq curInt(k, TRUE, diff) = diff + START .
eq curInt(k, FALSE, diff) = curInt(KEY_COMMIT, f(k), equals(KEY_COMMIT, f(k)), diff + ONE) .
eq geq(+(T_START, *(i, DUR)), +(curInt(k, TRUE, diff), *(DELAY, DUR))) = FALSE .
eq safeKey(k) = f(curInt(k, FALSE, ZERO) - DELAY) .
//eq safeKey(k) = f(curInt(k, FALSE, ZERO) - DELAY) .
Protocol
vars SName RName S1Name R1Name : Name .
......@@ -85,14 +85,14 @@ Protocol
// Receiver checks if f(i) is safe (still secret) by getting the current interval i from k1
// and ensuring the sender's current time (T_START + i * DUR) < i + (DELAY * DUR)
1. Sender -> Receiver : SName ; R1Name ; m1 ; mac(f(i), m1) ; f(i - DELAY)
|- S1Name ; RName ; m1 ; mac(k2, m) ; safeKey(k1) .
|- S1Name ; RName ; m1 ; mac(k2, m) ; f(curInt(k, FALSE, ZERO) - DELAY) .
// Sender sends packet in interval i+DELAY
// Sender dicloses key f(i)
// Receiver checks that the key is part of the key chain
// Receiver uses verifies that packet is safe
2. Sender -> Receiver : SName ; R1Name ; m2 ; mac(f(i + DELAY), m2) ; f(i)
|- S1Name ; RName ; m2 ; mac2 ; safeKey(k2) .
|- S1Name ; RName ; m2 ; mac2 ; k2 .
Out(Sender) = SName .
//Receiver uses k2 to authenticate message m1
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment