Commit b9513cd9 authored by Kayla Mesh's avatar Kayla Mesh

Added my changes in tesla-kayla.psl to compare with JoyDeep's changes in tesla.psl

parent 9b5536f8
spec TESLA is
Theory
types Name Nat Zero One NonZero Bool True False Key KeyMac Mac.
subtypes NonZero Zero Key < Nat .
subtypes One < NonZero .
subtypes True False < Bool .
ops T0 ZERO : -> Zero .
op ONE : -> One .
ops TS TR : -> Nat .
op TRUE : -> True .
op FALSE : -> False .
op _+_ : Nat Nat -> Nat [assoc comm id: ZERO] .
op _-_ : Nat Nat -> Nat .
op _*_ : Nat Nat -> Nat [assoc comm id: ONE] .
op leq : Nat Nat -> Bool [assoc] .
op equals : Nat Nat -> Bool [assoc comm] .
op geq : Nat Nat -> Bool [assoc] .
op Tfinal : Nat -> NonZero .
op TInit : Nat -> Nat .
// operations for sender setup
op DUR : -> NonZero . // Duration of interval
op LEN : -> NonZero . // Length of interval
op START : -> Nat . // Start time interval
op DELAY : -> Nat . // Delay
op KEY_COMMIT : -> Key . // Key commitment
// operations for key chain
op f : Nat -> Key .
op g : Key -> KeyMac .
op mac : Key Msg -> Mac .
//op mac : KeyMac Msg -> Mac .
op _^_ : Key Nat -> Key .
op _;_ : Msg Msg -> Msg [gather (e E)]. // Message concatenation
// variables for time
var u : NonZero .
vars w x y z : Nat .
var v : Nat .
vars tsrc trcv : Nat .
var m : Msg .
//equations about time
eq Tfinal(x) = +(T0,*(x,DUR)) .
eq TInit(u) = +(-(*(u,DUR),DUR)) .
eq TInit(ZERO) = T0 .
eq -(x,ZERO) = x .
eq equals(y,y) = TRUE .
eq equals(y,z) = FALSE .
eq leq(y,z) = equals(y,+(z,v)) .
eq geq(y,z) = leq(z,y) .
eq leq(ZERO,x) = TRUE .
eq leq(x,LEN) = TRUE .
eq leq(tsrc,+(trcv, -(TR,TS))) = TRUE .
eq geq(tsrc,+(TS, DELAY)) = FALSE .
// question - should we show that the key disclosure delay must be longer
// than the network propogation delay? (TR - TS)
//equations about key commitment
var c : Nat . // interval of the key commitment
eq geq(c, ZERO) = TRUE .
eq geq(c, START - DELAY) = FALSE .
eq KEY_COMMIT = f(c) .
//equations about key chain
eq leq(x,c) = FALSE .
eq geq(x,w) = FALSE .
eq leq(w,N) = TRUE .
eq f(x) = ^(f(w), -(w, x)) .
//eq g(x) = g(f(x)) .
Protocol
vars SName RName S1Name R1Name : Name .
// var i : Nat . i should be TS, i.e. the interval when the sender sends the packet
var m1 m2 : Msg .
var k1 k2 k3 : Key .
roles Sender Receiver .
In(Sender) = SName .
In(Receiver) = RName .
// Sender sends packet in interval (or TS)
// Receiver uses f(TS - DELAY) to determine TS - how ?
// Receiver checks that tsrc < TS + DELAY (since DELAY > trcv - TR)
1. Sender -> Receiver : SName ; R1Name ; m1 ; mac(f(TS), m1) ; f(TS - DELAY)
|- S1Name ; RName ; m1 ; mac(k2, m1) ; k1 .
// Receiver receives disclosed key f(TS)
// Receiver checks that f(TS) is the latest key received to date
// Receiver checks that f(TS) is a legitimate key in the key chain
// Receiver verifies that mac(k2, m1) = mac(f(TS), m1)
2. Sender -> Receiver : SName ; R1Name ; m2 ; mac(f(TS + DELAY), m2) ; f(TS)
|- S1Name ; RName ; m2 ; mac(k3, m2) ; k2 .
Out(Sender) = SName .
Out(Receiver) = RName, 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