diff --git a/README.md b/README.md
index 26c0b83..7f70033 100644
--- a/README.md
+++ b/README.md
@@ -1,2 +1,10 @@
 # Modeling Key Encapsulation Mechanisms in EasyCrypt
 
+EasyCrypt library that generically defines Key Encapsulation Mechanisms
+(KEMs), Public-Key Encryption (PKE) schemes, and their properties (both
+correctness and security), including the Random Oracle Model (ROM).  For
+convenience, it also provides some sensible defaults, particularly for
+oracles.  Most of the content is based on relevant literature.
+
+Includes generic instantiations of KEMs based on variation of the
+Fujisaki-Okamoto transform.