(****************************************************************************** * D A T A E N C R Y P T I O N S T A N D A R D *----------------------------------------------------------------------------- * INRIA - Unite de Recherche Rhone-Alpes * 655, avenue de l'Europe * 38330 Montbonnot Saint Martin * FRANCE *----------------------------------------------------------------------------- * Module : PERMUTATION_FUNCTIONS.lib * Auteur : Wendelin SERWE * Version : 1.3 * Date : 2015/08/18 17:16:07 *****************************************************************************) (* permutation functions required for the DES *) type PERMUTATION_FUNCTIONS is BIT32, BIT48, BIT56, BIT64 opns E : BIT32 -> BIT48 (* expansion *) IP : BIT64 -> BIT64 (* initial permutation *) IIP : BIT64 -> BIT64 (* inverse initial permutation *) P : BIT32 -> BIT32 (* permutation *) PC1 : BIT64 -> BIT56 (* permuted choice 1 *) PC2 : BIT56 -> BIT48 (* permuted choice 2 *) eqns forall B1, B2, B3, B4, B5, B6, B7, B8, B9, B10, B11, B12, B13, B14, B15, B16, B17, B18, B19, B20, B21, B22, B23, B24, B25, B26, B27, B28, B29, B30, B31, B32, B33, B34, B35, B36, B37, B38, B39, B40, B41, B42, B43, B44, B45, B46, B47, B48, B49, B50, B51, B52, B53, B54, B55, B56, B57, B58, B59, B60, B61, B62, B63, B64 : BIT ofsort BIT48 E (MK_32 (B1, B2, B3, B4, B5, B6, B7, B8, B9, B10, B11, B12, B13, B14, B15, B16, B17, B18, B19, B20, B21, B22, B23, B24, B25, B26, B27, B28, B29, B30, B31, B32)) = MK_48 (B32, B1, B2, B3, B4, B5, B4, B5, B6, B7, B8, B9, B8, B9, B10, B11, B12, B13, B12, B13, B14, B15, B16, B17, B16, B17, B18, B19, B20, B21, B20, B21, B22, B23, B24, B25, B24, B25, B26, B27, B28, B29, B28, B29, B30, B31, B32, B1); ofsort BIT32 P (MK_32 (B1, B2, B3, B4, B5, B6, B7, B8, B9, B10, B11, B12, B13, B14, B15, B16, B17, B18, B19, B20, B21, B22, B23, B24, B25, B26, B27, B28, B29, B30, B31, B32)) = MK_32 (B16, B7, B20, B21, B29, B12, B28, B17, B1, B15, B23, B26, B5, B18, B31, B10, B2, B8, B24, B14, B32, B27, B3, B9, B19, B13, B30, B6, B22, B11, B4, B25); ofsort BIT56 PC1 (MK_64 (B1, B2, B3, B4, B5, B6, B7, B8, B9, B10, B11, B12, B13, B14, B15, B16, B17, B18, B19, B20, B21, B22, B23, B24, B25, B26, B27, B28, B29, B30, B31, B32, B33, B34, B35, B36, B37, B38, B39, B40, B41, B42, B43, B44, B45, B46, B47, B48, B49, B50, B51, B52, B53, B54, B55, B56, B57, B58, B59, B60, B61, B62, B63, B64)) = MK_56 (B57, B49, B41, B33, B25, B17, B9, B1, B58, B50, B42, B34, B26, B18, B10, B2, B59, B51, B43, B35, B27, B19, B11, B3, B60, B52, B44, B36, B63, B55, B47, B39, B31, B23, B15, B7, B62, B54, B46, B38, B30, B22, B14, B6, B61, B53, B45, B37, B29, B21, B13, B5, B28, B20, B12, B4); ofsort BIT48 PC2 (MK_56 (B1, B2, B3, B4, B5, B6, B7, B8, B9, B10, B11, B12, B13, B14, B15, B16, B17, B18, B19, B20, B21, B22, B23, B24, B25, B26, B27, B28, B29, B30, B31, B32, B33, B34, B35, B36, B37, B38, B39, B40, B41, B42, B43, B44, B45, B46, B47, B48, B49, B50, B51, B52, B53, B54, B55, B56)) = MK_48 (B14, B17, B11, B24, B1, B5, B3, B28, B15, B6, B21, B10, B23, B19, B12, B4, B26, B8, B16, B7, B27, B20, B13, B2, B41, B52, B31, B37, B47, B55, B30, B40, B51, B45, B33, B48, B44, B49, B39, B56, B34, B53, B46, B42, B50, B36, B29, B32); ofsort BIT64 IP (MK_64 (B1, B2, B3, B4, B5, B6, B7, B8, B9, B10, B11, B12, B13, B14, B15, B16, B17, B18, B19, B20, B21, B22, B23, B24, B25, B26, B27, B28, B29, B30, B31, B32, B33, B34, B35, B36, B37, B38, B39, B40, B41, B42, B43, B44, B45, B46, B47, B48, B49, B50, B51, B52, B53, B54, B55, B56, B57, B58, B59, B60, B61, B62, B63, B64)) = MK_64 (B58, B50, B42, B34, B26, B18, B10, B2, B60, B52, B44, B36, B28, B20, B12, B4, B62, B54, B46, B38, B30, B22, B14, B6, B64, B56, B48, B40, B32, B24, B16, B8, B57, B49, B41, B33, B25, B17, B9, B1, B59, B51, B43, B35, B27, B19, B11, B3, B61, B53, B45, B37, B29, B21, B13, B5, B63, B55, B47, B39, B31, B23, B15, B7); ofsort BIT64 IIP (MK_64 (B1, B2, B3, B4, B5, B6, B7, B8, B9, B10, B11, B12, B13, B14, B15, B16, B17, B18, B19, B20, B21, B22, B23, B24, B25, B26, B27, B28, B29, B30, B31, B32, B33, B34, B35, B36, B37, B38, B39, B40, B41, B42, B43, B44, B45, B46, B47, B48, B49, B50, B51, B52, B53, B54, B55, B56, B57, B58, B59, B60, B61, B62, B63, B64)) = MK_64 (B40, B8, B48, B16, B56, B24, B64, B32, B39, B7, B47, B15, B55, B23, B63, B31, B38, B6, B46, B14, B54, B22, B62, B30, B37, B5, B45, B13, B53, B21, B61, B29, B36, B4, B44, B12, B52, B20, B60, B28, B35, B3, B43, B11, B51, B19, B59, B27, B34, B2, B42, B10, B50, B18, B58, B26, B33, B1, B41, B9, B49, B17, B57, B25); endtype (* ------------------------------------------------------------------------- *)