Commit a5f83a17 authored by Adrien KOUTSOS's avatar Adrien KOUTSOS

started to add for loop in processes

parent 2d8dd4bb
Pipeline #1637 passed with stage
in 1 minute and 57 seconds
let Voter[cid] sksig v pk =
new r0.
let ballot = enc(v,r0,pk) in
let zk = zkp(r0, v, ballot) in
out(cid, <<ballot,zk>,sign(<ballot, zk>, sksig)>);
let VoterA sksig v pk =
new r.
let ballot = enc(v,r,pk) in
let zk = zkp(r, v, ballot) in
out(ca, <<ballot,zk>,sign(<ballot, zk>, sksig)>);
let VoterB sksig v pk =
new r.
let ballot = enc(v,r,pk) in
let zk = zkp(r, v, ballot) in
out(cb, <<ballot,zk>,sign(<ballot, zk>, sksig)>);
let Outcome v1 v2 v3 sk =
(* We check for replayed ballots *)
if EQ(v1,v2) then
out(cres,replayedBallot())
else if EQ(v1,v3) then
......@@ -15,7 +19,6 @@ let Outcome v1 v2 v3 sk =
else if EQ(v2,v3) then
out(cres,replayedBallot())
else
(* No replay, we compute the result *)
let res1 = dec(v1,sk) in
let res2 = dec(v2,sk) in
let res3 = dec(v3,sk) in
......@@ -24,39 +27,39 @@ let Outcome v1 v2 v3 sk =
out(cres,<acount,bcount>);
letrec SubTally{i} v1 v2 v3 bv1 bv2 pksig1 pksig2 pksig3 sk =
let SubTally{i} v1 v2 v3 bv1 bv2 pksig1 pksig2 pksig3 sk =
in(c, x).
let content = pi1(x) in
if EQ(checksig(pi1(x),pi2(x),pksig1),sigok()) then
(if EQ(checkzkp(pi2(pi1(x)),pi1(pi1(x))),zkpok()) then
(SubTally
(SubTally{i-1}
(pi1(pi1(x))) v2 v3
true bv2
(A()) bv2
pksig1 pksig2 pksig3 sk)
else
(SubTally v1 v2 v3 bv1 bv2 pksig1 pksig2 pksig3 sk))
(SubTally{i-1} v1 v2 v3 bv1 bv2 pksig1 pksig2 pksig3 sk))
else if EQ(checksig(pi1(x),pi2(x),pksig2),sigok()) then
(if EQ(checkzkp(pi2(pi1(x)),pi1(pi1(x))),zkpok()) then
(SubTally
(SubTally{i-1}
v1 (pi1(pi1(x))) v3
bv1 true
bv1 (B())
pksig1 pksig2 pksig3 sk)
else
(SubTally v1 v2 v3 bv1 bv2 pksig1 pksig2 pksig3 sk))
(SubTally{i-1} v1 v2 v3 bv1 bv2 pksig1 pksig2 pksig3 sk))
else if EQ(checksig(pi1(x),pi2(x),pksig3),sigok()) then
(if EQ(checkzkp(pi2(pi1(x)),pi1(pi1(x))),zkpok()) then
(SubTally
(SubTally{i-1}
v1 v2 (pi1(pi1(x)))
bv1 bv2
pksig1 pksig2 pksig3 sk)
else
(SubTally v1 v2 v3 bv1 bv2 pksig1 pksig2 pksig3 sk))
(SubTally{i-1} v1 v2 v3 bv1 bv2 pksig1 pksig2 pksig3 sk))
else
(SubTally v1 v2 v3 bv1 bv2 pksig1 pksig2 pksig3 sk);
(SubTally{i-1} v1 v2 v3 bv1 bv2 pksig1 pksig2 pksig3 sk);
letrec SubTally{0} v1 v2 v3 bv1 bv2 pksig1 pksig2 pksig3 sk =
if bv1 then
(if bv2 then
let SubTally{0} v1 v2 v3 bv1 bv2 pksig1 pksig2 pksig3 sk =
if EQ(bv1,A()) then
(if EQ(bv2,B()) then
(Outcome v1 v2 v3 sk)
else
out(cres,badVotes()))
......@@ -83,7 +86,7 @@ let P vc1 vc2 =
out(cinit,sksig3).
((Vote[c1] sksig1 vc1 pk) | (Vote[c2] sksig2 vc2 pk)
| (SubTally{3} (N()) (N()) (N()) false false pksig1 pksig2 pksig3 sk));
((VoterA sksig1 vc1 pk) | (VoterB sksig2 vc2 pk)
| (SubTally{3} (N()) (N()) (N()) (C()) (C()) pksig1 pksig2 pksig3 sk));
goal: P (A()) (B()) ~ P (B()) (A())
......@@ -20,7 +20,8 @@ let parse_problem input_channel =
let (decl_list,(p_left,p_right)) =
Term_parser.problem Term_lexer.token lexbuf in
let _ = debug (fun () ->
Printf.eprintf "Parsed process %d declarations:\n" (List.length decl_list);
Printf.eprintf "Parsed process %d declarations:\n"
(List.length decl_list);
List.iter (fun process ->
print_process_decl Fmt.stderr process;
Fmt.pf Fmt.stderr "@.")
......@@ -280,8 +281,8 @@ let unit_test_encryption_oracle = fun () ->
(* Main Interactive Loop *)
(*************************)
unit_test_decryption_oracle ();
(* unit_test_decryption_oracle (); *)
unit_test_encryption_oracle ();
(* unit_test_encryption_oracle (); *)
main_interactive ();;
This diff is collapsed.
open Term
(* We only support public channels. *)
type channel = Public of string
type p_name_string = string
type p_name =
| Simple_proc of p_name_string
| Rec_proc of p_name_string * int
(* Type of processes. Mind the fact that in an Apply (s, l) the name s must be
binded to a process whose free variables are all bounded by the application
(i.e. after application the resulting process has no free variables). *)
type process =
| Nil
| Apply of string * msg term list
| Apply of p_name * msg term list
| New of string * process
| In of channel * string * process
| Out of channel * msg term * process
......@@ -16,17 +23,26 @@ type process =
| IfThenElse of boole term * process * process
| Let of string * msg term * process
(* Declaration of a parametrized process. PProcess (name, args_name, p) is the
process 'p', named 'name' and its free variable should be a subset of
args_name. *)
(* Declaration of a parametrized process.
- PProcess (name, args_name, p) is the declaration of the process 'p',
named 'name'. Its free variables must be a subset of args_name.
- PRec (name, args_name, pi, p0) is the declaration of the recursive
processes named name{x} (where x is an integer). Intuitively, this is a
primitive recursive definition: name{i}, for i>0, is 'pi', and can contain
name{i-1} as a sub-process; and name{0} is 'p0'.
The free variable of 'pi' and 'p0' must be a subset of args_name. *)
type declaration =
| PProcess of string * string list * process
| PProcess of p_name_string * string list * process
| PRec of p_name_string * string list * process * process
(* A recursive process declaration was badly done *)
exception Bad_rec_declaration of string
(* Apply (s,l) called on undefined parametrized process. *)
exception Undefined_process of string * int
exception Undefined_process of p_name
(* Apply (s,l) called on with the wrong number of arguments. *)
exception Bad_arity of string * int * int
exception Bad_arity of p_name * int * int
(* Remark: The folding algorithm used is only sound for action-deterministic
processes. We use an sound but cot complete algorithm to check whether the
......
......@@ -7,6 +7,7 @@
(* Nonce names and function names are distinguished by the presence of a parenthesis *)
let name = ['a'-'z' 'A'-'Z' '_'] ['a'-'z' 'A'-'Z' '0'-'9' '_']*
let int = ['0'-'9'] ['0'-'9']*
rule token = parse
| [' ' '\t' '\n'] (* ignore whitespace and tabs *)
......@@ -15,6 +16,10 @@ rule token = parse
{ LANGLE }
| '>'
{ RANGLE }
| '{'
{ LCURLY }
| '}'
{ RCURLY }
| ','
{ COMMA }
| "if"
......@@ -39,10 +44,14 @@ rule token = parse
{ PARALLEL }
| '='
{ EQUAL }
| '-'
{ MINUS }
| '~'
{ SIM }
| ';'
{ SEMICOLON }
| '1'
{ ONE }
| "let"
{ LET }
| "in"
......@@ -55,6 +64,8 @@ rule token = parse
{ GOAL }
| name as n
{ NAME (n) }
| int as j
{ INT (int_of_string j) }
| eof
{ EOF }
| _
......
%token <string> NAME
%token <int> INT
%token IF THEN ELSE
%token EQ
%token TRUE FALSE
......@@ -8,6 +9,7 @@
%token LANGLE RANGLE
%token IN NEW OUT LET EQUAL GOAL
%token PARALLEL DOT SIM SEMICOLON
%token LCURLY RCURLY MINUS ONE
%start term_list bterm_list problem
%type <Term.msg Term.term list> term_list
......@@ -18,18 +20,32 @@
%right ELSE
%%
(* Process Name *)
p_name_aux:
| i = NAME MINUS ONE
{ -2 }
| i = NAME
{ -1 }
| j = INT
{ j }
process_name:
| n = NAME
{ Process.Simple_proc(n) }
| n = NAME LCURLY j = p_name_aux RCURLY
{ Process.Rec_proc(n,j) }
(* Terms *)
term_list:
| t = term l = term_list
{ t :: l }
| t = term EOF
| t = term EOF
{ [t] }
bterm_list:
| b = bterm l_b = bterm_list
{ b :: l_b }
| b = bterm EOF
| b = bterm EOF
{ [b] }
bterm:
......@@ -75,13 +91,13 @@ apply_arg:
process:
| LPAREN p = process RPAREN
{ p }
| id = NAME args = apply_arg
| id = process_name args = apply_arg
{ Process.Apply (id, args) }
| NEW s = NAME DOT p = process
{ Process.New (s, p) }%prec PARALLEL
| IN LPAREN c = NAME COMMA s = NAME RPAREN DOT p = process
{ Process.In (Process.Public c, s, p) }%prec PARALLEL
| IN LPAREN c = NAME COMMA s = NAME RPAREN
| IN LPAREN c = NAME COMMA s = NAME RPAREN
{ Process.In (Process.Public c, s, Process.Nil) }
| OUT LPAREN c = NAME COMMA t = term RPAREN DOT p = process
{ Process.Out (Process.Public c, t, p) }%prec PARALLEL
......@@ -105,6 +121,22 @@ arg_list:
declaration:
| LET s = NAME l = arg_list p = process SEMICOLON
{ Process.PProcess (s, l, p) }
| LET s1 = NAME LCURLY i1 = p_name_aux RCURLY
l1 = arg_list p1 = process SEMICOLON
LET s2 = NAME LCURLY i2 = p_name_aux RCURLY
l2 = arg_list p2 = process SEMICOLON
{ if (s1 <> s2) || (l1 <> l2) then
raise (Process.Bad_rec_declaration
(Printf.sprintf "%s %s %d %d"
s1 s2 (List.length l1) (List.length l2)))
else if (i1 = -1) && (i2 = 0) then
Process.PRec (s1, l1, p1,p2)
else if (i1 = 0) && (i2 = -1) then
Process.PRec (s1, l2, p2,p1)
else
raise (Process.Bad_rec_declaration
(Printf.sprintf "%s %d %d"
s1 i1 i2))}
declaration_list:
| d = declaration l = declaration_list
......
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