Changeset 16158
 Timestamp:
 12/05/08 10:27:49 (8 years ago)
 Files:

 5 edited
Legend:
 Unmodified
 Added
 Removed

processes/old/daajoin.spi
r13094 r16158 1 1 (** Direct Anonymous Attestation (DAA)  Join Protocol *) 2 2 3 statement sjoin(*2,4*) = landh( eqh(blind(alpha(*1*), alpha(*2*)), beta(*2*)), eqh(hash(pair(beta(*4*), alpha(*1*))), beta(*3*)) ) (*: Stm(Pair(yid : Un, Pair(yu : Blind(Private), Pair(yn : Un, Pair(yxi : Un, Ok [*# exists([x1,x2], and( equal(yu,blind(x1,x2)), equal(yn,hash(pair(yxi,x1))) ))*]))))) *). 3 statement sjoin(*2,4*) = landh( eqh(blind(alpha(*1*), alpha(*2*)), beta(*2*)), eqh(hash(pair(beta(*4*), alpha(*1*))), beta(*3*)) ) 4 (*: Stm(yid : Un, yu : Blind(Private), yn : Un, yxi : Un; [*# exists([x1,x2], and( equal(yu,blind(x1,x2)), equal(yn,hash(pair(yxi,x1))) ))*]) *). 4 5 5 6 predicate ValidTPM(*1*). … … 18 19 new r (*: Blinder(Private) *); 19 20 (assume(*#Join(tid, blind(f,r))*)  20 out(c1,zk(*2,4,sjoin*)(f,r,tid,blind(f,r),hash(pair(hash(pair(n1 (*=d6*), bsni(*: Untainted *)))(*=y*),f(*: Private*))),hash(pair(n1(*=d7*), bsni(*: Untainted*)))));21 out(c2,pair( tid(*=xid*),pair(blind(f,r)(*=xu*),ok(*:Ok [*# Join(xid, xu) *]*)) (*:Pair(yu : Blind(Private), Ok [*#Join(xid, yu)*])*) ));21 out(c1,zk(*2,4,sjoin*)(f,r,tid,blind(f,r),hash(pair(hash(pair(n1, bsni(*: Un *))),f(*: Private*))),hash(pair(n1, bsni(*: Un *))))); 22 out(c2,pair((*=xid*)tid,pair((*=xu*)blind(f,r),ok(*:Ok [*# Join(xid, xu) *]*)) (*:Pair(yu : Blind(Private), Ok [*#Join(xid, yu)*])*) )); 22 23 in(c3, x); 23 24 let cert = unblind(*:Pair(yu : Blind(Private), Ok [*# exists([xid],Certified(xid,yu)) *])*)(x, r, bvk(ki)) in 24 25 let tt = bcheck(*:Pair(yu : Blind(Private), Ok [*# exists([xid],Certified(xid,yu)) *])*)(cert, bvk(ki)) in 25 let xu = fst(tt)in26 let (xu, o) = tt in 26 27 let d1 = eq(xu, f) in 27 let o = snd(tt) in28 let d2 = exercise(o) in29 28 assert(*#Joined(tid,f,blind(f,r))*) 30 29 ). … … 34 33 !in(c1,xzk); 35 34 in(c2,ttt); 36 let yid = fst(ttt) in 37 let tt = snd(ttt) in 38 let yu = fst(tt) in 39 let o1 = snd(tt) in 40 let d1 = exercise(o1) in 41 let o2 = ver(*2,4,4,sjoin*)(xzk, yid, yu, hash(pair(hash(pair(n1(*=d2*), bsni(*: Untainted *)))(*=d*),f(*:Private*))), pair(n1(*=d8*), bsni(*: Untainted *))) in 42 let d2 = exercise(o2) in 35 let (yid, tt) = ttt in 36 let (yu, o1) = tt in 37 let o2 = ver(*2,4,4,sjoin*)(xzk, yid, yu, hash(pair(hash(pair(n1, bsni(*: Un *))),f(*:Private*))), pair(n1, bsni(*: Un *))) in 43 38 (assert(*#Certified(yid,yu)*)  44 out(c3, bsign(*:Pair(yu : Blind(Private), Ok [*# exists([xid],Certified(xid,yu)) *])*)(pair( yu(*=x*),ok(*: Ok [*# exists([xid],Certified(xid,yu)) *]*)), ki))39 out(c3, bsign(*:Pair(yu : Blind(Private), Ok [*# exists([xid],Certified(xid,yu)) *])*)(pair((*=x*)yu,ok(*: Ok [*# exists([xid],Certified(xid,yu)) *]*)), ki)) 45 40 ). 46 41 47 42 process 48 new c2 (*: Ch Pair(yid : Un, Pair(yu : Blind(Private), Ok [*#Join(yid, yu)*]))*);49 new bsni (*: Un tainted*);43 new c2 (*: Ch(Pair(yid : Un, Pair(yu : Blind(Private), Ok [*#Join(yid, yu)*] )))*); 44 new bsni (*: Un *); 50 45 new daaseed (*: Private *); 51 46 new f (*: Private *); (** cutting corners for now *) 
processes/old/daa.spi
r13094 r16158 1 1 (** Direct Anonymous Attestation (DAA) *) 2 2 3 statement sjoin(*2,4*) = landh( eqh(blind(alpha(*1*), alpha(*2*)), beta(*2*)), eqh(hash(pair(beta(*4*), alpha(*1*))), beta(*3*)) ) (*: Stm(Pair(yid : Un, Pair(yu : Blind(Private), Pair(yn : Un, Pair(yxi : Un, Ok [*# exists([x1,x2], and( equal(yu,blind(x1,x2)), equal(yn,hash(pair(yxi,x1))) ))*]))))) *). 3 statement sjoin(*2,4*) = landh( eqh(blind(alpha(*1*), alpha(*2*)), beta(*2*)), eqh(hash(pair(beta(*4*), alpha(*1*))), beta(*3*)) ) 4 (*: Stm(yid : Un, yu : Blind(Private), yn : Un, yxi : Un; [*# exists([x1,x2], and( equal(yu,blind(x1,x2)), equal(yn,hash(pair(yxi,x1))) ))*]) *). 4 5 5 6 statement ssign(*2,4*) = 6 7 landh(eqh(bcheckh(alpha(*2*), beta(*1*)), alpha(*1*)), 7 8 eqh(hash(pair(beta(*3*),alpha(*1*))), beta(*2*))) 8 (*: Stm( Pair(9 yvk : BlindVerKey(Pair(yu : Blind(Private), Ok [*#exists([xid],Certified(xid,yu))*])), Pair(10 yn : Un, Pair(11 yxi : Un, Pair(12 ym : Un ,13 Ok [*#exists([xf,xcert,xv,xbs,xid], and(and(equal(yn,hash(pair(yxi,xf))), Certified(xid,blind(xf,xv))),DSigned(xf,ym)))*])))))9 (*: Stm( 10 yvk : BlindVerKey(Pair(yu : Blind(Private), Ok [*#exists([xid],Certified(xid,yu))*])), 11 yn : Un, 12 yxi : Un, 13 ym : Un; 14 [*#exists([xf,xcert,xv,xbs,xid], and(and(equal(yn,hash(pair(yxi,xf))), Certified(xid,blind(xf,xv))),DSigned(xf,ym)))*]) 14 15 *). 15 16 … … 35 36 new r (*: Blinder(Private) *); 36 37 (assume(*#Join(tid, blind(f,r))*)  37 out(c1,zk(*2,4,sjoin*)(f,r,tid,blind(f,r),hash(pair(hash(pair(n1 (*=d6*), bsni(*: Untainted *)))(*=y*),f(*: Private*))),hash(pair(n1(*=d7*), bsni(*: Untainted*)))));38 out(c2,pair( tid(*=xid*),pair(blind(f,r)(*=xu*),ok(*:Ok [*# Join(xid, xu) *]*)) (*:Pair(yu : Blind(Private), Ok [*#Join(xid, yu)*])*) ));38 out(c1,zk(*2,4,sjoin*)(f,r,tid,blind(f,r),hash(pair(hash(pair(n1, bsni(*: Un *))),f(*: Private*))),hash(pair(n1, bsni(*: Un *))))); 39 out(c2,pair((*=xid*)tid,pair((*=xu*)blind(f,r),ok(*:Ok [*# Join(xid, xu) *]*)) (*:Pair(yu : Blind(Private), Ok [*#Join(xid, yu)*])*) )); 39 40 in(c3, xbs); 40 41 let cert = unblind(*:Pair(yu : Blind(Private), Ok [*# exists([xid],Certified(xid,yu)) *])*)(xbs, r, bvk(ki)) in 41 42 let tt = bcheck(*:Pair(yu : Blind(Private), Ok [*# exists([xid],Certified(xid,yu)) *])*)(cert, bvk(ki)) in 42 let xu = fst(tt)in43 let (xu, o) = tt in 43 44 let d1 = eq(xu, f) in 44 let o = snd(tt) in45 let d2 = exercise(o) in46 45 (assert(*#Joined(tid,f,blind(f,r))*)  47 46 48 47 (** Sign *) 49 new m (*: Un tainted*);48 new m (*: Un *); 50 49 new xi (*: Un *); 51 50 (assume(*#DSigned(f,m)*)  52 out(c4, zk(*2,4,ssign*)(f, cert, bvk(ki), hash(pair(xi (*=d2*),f(*: Private *))), xi, m))51 out(c4, zk(*2,4,ssign*)(f, cert, bvk(ki), hash(pair(xi,f(*: Private *))), xi, m)) 53 52 ))). 54 53 … … 57 56 !in(c1,xzk); 58 57 in(c2,ttt); 59 let yid = fst(ttt) in 60 let tt = snd(ttt) in 61 let yu = fst(tt) in 62 let o1 = snd(tt) in 63 let d1 = exercise(o1) in 64 let o2 = ver(*2,4,4,sjoin*)(xzk, yid, yu, hash(pair(hash(pair(n1(*=d2*), bsni(*: Untainted *)))(*=d*),f(*:Private*))), pair(n1(*=d8*), bsni(*: Untainted *))) in 65 let d2 = exercise(o2) in 58 let (yid, tt) = ttt in 59 let (yu, o1) = tt in 60 let o2 = ver(*2,4,4,sjoin*)(xzk, yid, yu, hash(pair(hash(pair(n1, bsni(*: Un *))),f(*:Private*))), pair(n1, bsni(*: Un *))) in 66 61 (assert(*#Certified(yid,yu)*)  67 out(c3, bsign(*:Pair(yu : Blind(Private), Ok [*# exists([xid],Certified(xid,yu)) *])*)(pair( yu(*=yu*),ok(*: Ok [*# exists([xid],Certified(xid,yu)) *]*)), ki))62 out(c3, bsign(*:Pair(yu : Blind(Private), Ok [*# exists([xid],Certified(xid,yu)) *])*)(pair((*=yu*)yu,ok(*: Ok [*# exists([xid],Certified(xid,yu)) *]*)), ki)) 68 63 ). 69 64 … … 71 66 !in(c4, xzks); 72 67 let tttt = ver(*2,4,1,ssign*)(xzks,bvk(ki)) in 73 let xn = fst(tttt) in 74 let ttt = snd(tttt) in 75 let xxi = fst(ttt) in 76 let tt = snd(ttt) in 77 let xm = fst(tt) in 78 let o = snd(tt) in 79 let d = exercise(o) in 68 let (xn, ttt) = tttt in 69 let (xxi, tt) = ttt in 70 let (xm, o) = tt in 80 71 assert(*#Authenticated(xm)*). 81 72 82 73 process 83 new c2 (*: Ch Pair(yid : Un, Pair(yu : Blind(Private), Ok [*#Join(yid, yu)*]))*);84 new bsni (*: Un tainted*);74 new c2 (*: Ch(Pair(yid : Un, Pair(yu : Blind(Private), Ok [*#Join(yid, yu)*])))*); 75 new bsni (*: Un *); 85 76 new daaseed (*: Private *); 86 77 new f (*: Private *); (** cutting corners for now *) 
processes/old/proxy.spi
r13095 r16158 11 11 new song(*:Un*); 12 12 (assume(*#Order(u,song)*)  13 out(c, sign(pair( song(*=s*),ok(*:Ok[*#Order(u,s)*]*)),ku))).13 out(c, sign(pair((*=s*)song,ok(*:Ok[*#Order(u,s)*]*)),ku))). 14 14 15 15 let proxy = … … 17 17 !in(c,m); 18 18 let p = check(m,vk(ku)) in 19 let s = fst(p) in 20 let o = snd(p) in 21 let d = exercise(o) in 22 out(c, sign(pair(u(*=u1*),pair(s(*=s1*),ok(*:Ok[*#and(Order(u1,s1),Registered(u1))*]*))(*:Pair(s1:Un,Ok[*#and(Order(u1,s1),Registered(u1))*])*)), kp)). 19 let (s, o) = p in 20 out(c, sign(pair((*=u1*)u,pair((*=s1*)s,ok(*:Ok[*#and(Order(u1,s1),Registered(u1))*]*))(*:Pair(s1:Un,Ok[*#and(Order(u1,s1),Registered(u1))*])*)), kp)). 23 21 24 22 let store = 25 23 !in(c,x); 26 24 let ttt = check(x,vk(kp)) in 27 let u = fst(ttt) in 28 let tt = snd(ttt) in 29 let s = fst(tt) in 30 let o = snd(tt) in 31 let d = exercise(o) in 25 let (u, tt) = ttt in 26 let (s, o) = tt in 32 27 assert(*#CanDownload(u,s)*). 33 28 
processes/old/sign.spi
r13094 r16158 8 8 in(c, m); 9 9 (assume (*#Good(m)*)  10 out(c, sign(pair( m(*=x*),ok(*:Ok [*#Good(x)*]*)), ks))10 out(c, sign(pair((*=x*)m,ok(*:Ok [*#Good(x)*]*)), ks)) 11 11 ). 12 12 … … 14 14 !in(c, y); 15 15 let m = check(y, vk(ks)) in 16 let z = fst(m) in 17 let p = snd(m) in 18 let dummy = exercise(p) in 16 let (z, p) = m in 19 17 assert (*#Good(z)*). 20 18 … … 22 20 !in(c, y); 23 21 let m = check(y, vk(ks)) in 24 let z = fst(m) in 25 let p = snd(m) in 26 let dummy = exercise(p) in 22 let (z, p) = m in 27 23 assert (*#Good(z)*). 28 24 
src/typechecker/parser.mly
r16157 r16158 244 244  IDENT LPAREN STAR COLON typedef STAR RPAREN { Ident($1, Some $5) } 245 245  PAIR LPAREN LPAREN STAR EQUAL IDENT STAR RPAREN term COMMA term LPAREN STAR COLON typedef STAR RPAREN RPAREN 246 { Pair($9, Some $6, $11, Some($15)) } 247  PAIR LPAREN LPAREN STAR EQUAL IDENT STAR RPAREN term COMMA term RPAREN { Pair($9, Some $6, $11, None) } 246 { Pair($9, Some $6, $11, Some $15) } 247  PAIR LPAREN term COMMA term LPAREN STAR COLON typedef STAR RPAREN RPAREN 248 { Pair($3, None, $5, Some $9) } 249  PAIR LPAREN LPAREN STAR EQUAL IDENT STAR RPAREN term COMMA term RPAREN 250 { Pair($9, Some $6, $11, None) } 251  PAIR LPAREN term COMMA term RPAREN 252 { Pair($3, None, $5, None) } 248 253  constr LPAREN STAR COLON typedef STAR RPAREN { Constr($1, Some $5) } 249 254  constr { Constr($1, None) }
Note: See TracChangeset
for help on using the changeset viewer.