...
 
Commits (3)
.DS_Store
spec TESLA is
Theory
types Nat Zero One NonZero Bool True False Key KeyMAC.
types Name Nat Zero One NonZero Bool True False Key KeyMAC Enc .
type SecretKey .
subtypes NonZero Zero Key < Nat .
subtypes One < NonZero .
subtypes True False < Bool .
......@@ -12,6 +13,9 @@ 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] .
......@@ -22,17 +26,29 @@ Theory
op Tfinal : Nat -> NonZero .
op TInit : Nat -> Nat .
op START : -> Nat . // Start time interval
op DELAY : -> Nat . // Delay
op f : Nat -> Key .
op g : Key -> KeyMAC .
op _^_ : Key Nat -> Key .
op _;_ : Msg Msg -> Msg .
var u : NonZero .
vars x y z : Nat .
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)) .
eq TInit(u) = +(-(*(u,D),D)) .
eq TInit(ZERO) = T0 .
eq -(x,ZERO) = x .
eq equals(y,y) = TRUE .
eq equals(z,z) = TRUE . // Do we need this ?
eq equals(y,z) = FALSE .
eq leq(y,z) = equals(y,+(z,v)) .
eq geq(y,z) = leq(z,y) .
......@@ -40,19 +56,26 @@ Theory
eq leq(x,N) = TRUE .
eq leq(tsrc,+(trcv, -(TR,TS))) = TRUE .
// Sender setup
op key_commit : -> Key .
op s : -> Nat . // Start time interval
op d : -> Nat . // Delay
op f : Nat -> Key .
op g : Key -> KeyMAC .
op _^_ : Key Nat -> Key .
op _;_ : Msg Msg -> Msg .
eq key_commit = f(s - d) .
eq f(x) = ^(f(N), -(N, x)) .
eq f(s - d) = ^(f(x), -(+(i,d),s) .
//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 .
roles Sender Receiver .
In(Receiver) = RName sk .
In(Sender) = SName, RName, sk .
Def(Sender) = sched1 := D ; START ; TInit(START) ; N ,
sched2 := DELAY ,
sched3 := f(i) .
\ No newline at end of file
1 . Sender -> Receiver : SName ; RName ; enc(sk, sched1 ; sched2 ; sched3) |- S1Name ; RNAME ; em .
2. Receiver -> Sender : S1Name ; RName