Commit e67c0ac1 authored by Joy Mitra's avatar Joy Mitra
Browse files

tesla protocol

parent dc772c68
spec TESLA is
Theory
types Name Nat Zero One NonZero Bool True False Key KeyMAC Enc .
type SecretKey .
types Name Nat Zero One NonZero Bool True False Key KeyMAC .
subtypes NonZero Zero Key < Nat .
subtypes One < NonZero .
subtypes True False < Bool .
......@@ -13,35 +12,32 @@ Theory
op TRUE : -> True .
op FALSE : -> False .
op enc : SecretKey Msg -> Enc .
op dec : SecretKey Enc -> Msg .
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 not : Bool -> Bool .
op and : Bool Bool -> Bool [assoc comm] .
op Tfinal : Nat -> NonZero .
op TInit : Nat -> Nat .
op START : -> Nat . // Start time interval
op DELAY : -> Nat . // Delay
op DELAY : -> NonZero . // Delay
op KEY_COMMIT_INT : -> Nat .
op f : Nat -> Key .
op mac : Key Msg -> Msg .
op g : Key -> KeyMAC .
op _^_ : Key Nat -> Key .
op _;_ : Msg Msg -> Msg .
op _;_ : Msg Msg -> Msg [gather (e E)] .
var u : NonZero .
vars w x y z : Nat .
var v : Nat .
vars tsrc trcv : Nat .
var m : Msg .
var sec : SecretKey .
//equation about symmetric encryption
eq dec(sec,enc(sec,m)) = m
//equations about time
eq Tfinal(x) = +(T0,*(x,D)) .
......@@ -55,27 +51,35 @@ Theory
eq leq(ZERO,x) = TRUE .
eq leq(x,N) = TRUE .
eq leq(tsrc,+(trcv, -(TR,TS))) = TRUE .
eq geq(KEY_COMMIT_INT,-(START,DELAY)) = FALSE .
eq not(TRUE) = FALSE .
eq not(FALSE) = TRUE .
eq and(TRUE,TRUE) = TRUE .
eq and(TRUE,FALSE) = FALSE .
eq and(FALSE,TRUE) = FALSE .
eq and(FALSE,FALSE) = FALSE .
//equations about key chain
eq geq(x,w) = FALSE .
eq leq(w,N) = TRUE .
eq f(x) = ^(f(w), -(w, x)) .
//eq f(START - DELAY) = ^(f(x), -(+(i,DELAY),START) . //Think about this later
Protocol
vars SName RName S1Name R1Name : Name .
var i : Nat .
var sk : SecretKey
var em : Enc .
vars i x j : Nat .
var k : Key .
vars m m1 : Msg .
roles Sender Receiver .
In(Receiver) = RName sk .
In(Sender) = SName, RName, sk .
In(Receiver) = RName .
In(Sender) = SName, RName .
Def(Sender) = sched1 := D ; START ; TInit(START) ; N ,
sched2 := DELAY ,
sched3 := f(i) .
1 . Sender -> Receiver : SName ; R1Name ; m ; mac(f(i),m); f(i-DELAY)
|- S1Name ; RName ; m ; m1; k .
1 . Sender -> Receiver : SName ; RName ; enc(sk, sched1 ; sched2 ; sched3) |- S1Name ; RNAME ; em .
2. Receiver -> Sender : S1Name ; RName
Out(Sender) = SName, RName .
Out(Receiver) = i, and(TRUE,not(geq(x,+(i,DELAY)))),
and(TRUE,not(geq(i,j))),
and(TRUE,equals(k,f(i-DELAY))),
and(TRUE,not(geq(v,i))),
and(TRUE,equals(f(v),^(f(i), -(i, v)))) .
Supports Markdown
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