|
|
|
@58167
|
4 months |
hritcu |
Old stuff from my Mac
|
|
|
|
@43428
|
17 months |
hritcu |
Thorsten's patch for building the spi-calculus parser for F5's Spi2RCF …
|
|
|
|
@37033
|
23 months |
pecina |
fixed forgotten printf
|
|
|
|
@37031
|
23 months |
pecina |
further cleaned up the code and removed leftover printf
|
|
|
|
@37029
|
23 months |
pecina |
fixed killing issues with the spass and e option
- solution was to put the …
|
|
|
|
@37026
|
23 months |
pecina |
worked some more on the spass and e option (still does not work as …
|
|
|
|
@37018
|
23 months |
mohammadi |
|
|
|
|
@37009
|
23 months |
pecina |
performed some code cleaning
moved the fprintf error messages into …
|
|
|
|
@36949
|
23 months |
pecina |
fixed errors in d2c config file
|
|
|
|
@36947
|
23 months |
pecina |
added an extra file for d2c
|
|
|
|
@36398
|
2 years |
pecina |
finished implementing the solution for both, spass and e, simultaneously …
|
|
|
|
@36392
|
2 years |
pecina |
modified the type checker to allow for more easy extensions of the …
|
|
|
|
@33221
|
2 years |
pecina |
added a config file for ring signatures and group encryptions
added a …
|
|
|
|
@31895
|
2 years |
reischuk |
* new type: Tag
* new constructors of type Tag: lft() and rgt()
|
|
|
|
@31339
|
2 years |
pecina |
accomodated the template spass for empty forall constructs (removed) …
|
|
|
|
@31338
|
2 years |
pecina |
changed the name of type bool to Bool and the constructors are now called …
|
|
|
|
@31336
|
2 years |
hritcu |
tabs
|
|
|
|
@31335
|
2 years |
hritcu |
Fixed genckind to allow nullary type constructors.
|
|
|
|
@31334
|
2 years |
pecina |
chanced the default config to include bools, fixed accordingly for …
|
|
|
|
@31322
|
2 years |
hritcu |
Some of the tests involved in finding the last bug.
|
|
|
|
@31321
|
2 years |
hritcu |
Fix for the bug in sub (the right fix!)
|
|
|
|
@31320
|
2 years |
hritcu |
One more horrible bug in sub -- this time it was helping Kim too much :)
|
|
|
|
@31313
|
2 years |
hritcu |
Added command line flag to not delete temp files holding successfully …
|
|
|
|
@31311
|
2 years |
hritcu |
proc_case was blindly trusting annotation
|
|
|
|
@30960
|
2 years |
hritcu |
Fixed spassparser.mly to accept nullary function symbols (Ticket #100)
|
|
|
|
@30941
|
2 years |
hritcu |
Fixed spassprint.ml (Ticket #100)
|
|
|
|
@30940
|
2 years |
hritcu |
one more sample using lists
|
|
|
|
@30934
|
2 years |
hritcu |
Allowing the user to annotate polymorphic nullary constructors (Ticket …
|
|
|
|
@30931
|
2 years |
hritcu |
Fixed gentemplate.ml (Ticket #100)
|
|
|
|
@30926
|
2 years |
hritcu |
Support zero-arity constructors (constants) -- Ticket #100
|
|
|
|
@29236
|
2 years |
eigner |
fixed critical bug in parser, removed let constructor else
|
|
|
|
@28320
|
2 years |
pecina |
change one more thing in the parser to read an else always to the directly …
|
|
|
|
@28301
|
2 years |
pecina |
the parser now reads processes gready and parallel processes now have the …
|
|
|
|
@27977
|
2 years |
hritcu |
Fixed bugs in generator code handling type constructors with more than one …
|
|
|
|
@27975
|
2 years |
eigner |
|
|
|
|
@27964
|
2 years |
eigner |
added randomized pk crypto with reencryption to calc, to use this call …
|
|
|
|
@27859
|
2 years |
eigner |
|
|
|
|
@27858
|
2 years |
eigner |
added config file for spi with lists and modified makefile accordingly
|
|
|
|
@27268
|
2 years |
hritcu |
Fixed horrible bug in sub that was hurting Kim.
|
|
|
|
@27120
|
2 years |
pecina |
it is now possible to have nested comments:
( (* asdf*)fads *) is all …
|
|
|
|
@23964
|
3 years |
hritcu |
Updated to F# 1.9.6.16
|
|
|
|
@23953
|
3 years |
tarrach |
i guess i should have commited that earlier
|
|
|
|
@18724
|
3 years |
broeni |
got rid of most of the duplicated code concerning the checkers in …
|
|
|
|
@18723
|
3 years |
broeni |
changed new a little bit
|
|
|
|
@18716
|
3 years |
broeni |
base work for the non-dup checker file
|
|
|
|
@18462
|
3 years |
hritcu |
Added support for time-outs -- for SPASS and eprover (fixes Ticket #49). …
|
|
|
|
@18414
|
3 years |
hritcu |
Made the compile have linear complexity by discharging obligations on the …
|
|
|
|
@18359
|
3 years |
hritcu |
Changed compile so that we no longer do type inference and use the type …
|
|
|
|
@18358
|
3 years |
hritcu |
Big change coming soon
|
|
|
|
@18350
|
3 years |
hritcu |
Added support for linear statement processing (fixes Ticket #85)
|
|
|
|
@18346
|
3 years |
hritcu |
Lazily evaluating "pub", "tnt", "sub" and "non_disj" in zk verification …
|
|
|
|
@18345
|
3 years |
tarrach |
fixed fs side
|
|
|
|
@18344
|
3 years |
hritcu |
Started working on Ticket #71 + some leftovers from Ticket #79
|
|
|
|
@18342
|
3 years |
hritcu |
Change everything to the new FOL syntax (no longer using the ugly spass …
|
|
|
|
@18316
|
3 years |
hritcu |
Supporting dependent zero-knowledge proof types (Ticket #84)
|
|
|
|
@18238
|
3 years |
tarrach |
fixes fs side
|
|
|
|
@18235
|
3 years |
hritcu |
The "public" destructor was not handled properly when I implemented the …
|
|
|
|
@18209
|
3 years |
hritcu |
Fixed severe bug in create_fresh_name (Ticket #80)
|
|
|
|
@18206
|
3 years |
hritcu |
Added test case exhibiting (Ticket #80)
|
|
|
|
@18182
|
3 years |
hritcu |
Stopped annotating "zk"-s and "ver"-s with redundant arity information …
|
|
|
|
@18179
|
3 years |
hritcu |
Added the number of matched components to the statement definition (Ticket …
|
|
|
|
@18133
|
3 years |
hritcu |
|
|
|
|
@18069
|
3 years |
hritcu |
Supporting types for the secret components of a zero-knowledge proof …
|
|
|
|
@17982
|
3 years |
hritcu |
Fixed incorrect implementation of non-disjoint and statement compilation …
|
|
|
|
@17710
|
3 years |
hritcu |
|
|
|
|
@17698
|
3 years |
broeni |
fixed the problem introduced in checker.ml in my last change. blame me
|
|
|
|
@17693
|
3 years |
hritcu |
Ugly hack
|
|
|
|
@17677
|
3 years |
tarrach |
spi2rcf config file
|
|
|
|
@17626
|
3 years |
broeni |
dramatically reduced the usage of list2set by making dom return a set …
|
|
|
|
@17608
|
3 years |
tarrach |
|
|
|
|
@17580
|
3 years |
hritcu |
|
|
|
|
@17550
|
3 years |
tarrach |
cross-compiling working again
|
|
|
|
@17184
|
3 years |
hritcu |
Fixed samples
|
|
|
|
@17183
|
3 years |
broeni |
changed printing of parallel to be more expressive, changed the type of …
|
|
|
|
@17169
|
3 years |
hritcu |
Sample exhibiting bug
|
|
|
|
@17047
|
3 years |
hritcu |
Added more cases to non-disjoint (not sure they are sound), added one more …
|
|
|
|
@17015
|
3 years |
hritcu |
Changed daa-sign-simplified.spi so that it exercises the fix to Ticket …
|
|
|
|
@17013
|
3 years |
broeni |
tracked the bug from ticket #75. Used replace_formula instead of the old …
|
|
|
|
@17010
|
3 years |
hritcu |
Fixed simple-zk-encoded.spi
|
|
|
|
@16990
|
3 years |
hritcu |
Committed the wrong file before ... simple-zk-encoded.spi doesn't really …
|
|
|
|
@16989
|
3 years |
hritcu |
Added simplified version of the DAA-sign protocol where the zero-knowledge …
|
|
|
|
@16988
|
3 years |
hritcu |
Added simplified version of the DAA-sign protocol where the zero-knowledge …
|
|
|
|
@16987
|
3 years |
hritcu |
Added simplified version of the DAA-sign protocol -- used in the slides
|
|
|
|
@16980
|
3 years |
hritcu |
Added example that shows that having Hash(Private) tainted would be …
|
|
|
|
@16976
|
3 years |
hritcu |
Example for union types -- nounce handshake using public-key encryption
|
|
|
|
@16729
|
3 years |
hritcu |
Fixed printing ands and ors
|
|
|
|
@16679
|
3 years |
broeni |
got rid of all warnings. In most cases only an exception is risen. This is …
|
|
|
|
@16678
|
3 years |
broeni |
removed more warnings
|
|
|
|
@16660
|
3 years |
hritcu |
- Implemented destructor reduction as a relation (Ticket #65)
- Changed …
|
|
|
|
@16621
|
3 years |
hritcu |
Fixed alpha-renaming problem when type-checking dependent pairs (we were …
|
|
|
|
@16575
|
3 years |
broeni |
removed first warnings
|
|
|
|
@16567
|
3 years |
hritcu |
Statement compilation can now reason about public keys: added "\alpha_n = …
|
|
|
|
@16566
|
3 years |
hritcu |
Fixed Ticket #64: when breaking tuples always check that the last …
|
|
|
|
@16565
|
3 years |
hritcu |
Fixed spass2fol: more than one variable could be quantified at the same …
|
|
|
|
@16554
|
3 years |
broeni |
it is a little bit nasty, but now, if an error occurs in make clean, it is …
|
|
|
|
@16542
|
3 years |
hritcu |
Attempt to fix Ticket #62: Added injectivity and pairwise distinctness of …
|
|
|
|
@16438
|
3 years |
grochulla |
extended default.config with symmetric key cryptography
|
|
|
|
@16384
|
3 years |
broeni |
heavily changed the makefile. Not completely done yet. but all .cmo and …
|
|
|
|
@16361
|
3 years |
hritcu |
Changed kinding zkproof types to match paper
|
|
|
|
@16358
|
3 years |
hritcu |
Added a sample exemplifying bug #58
|
|
|
|
