-
Formally-verified Security against Forgery of Remote Attestation using SSProve
Authors:
Sara Zain,
Jannik Mähn,
Stefan Köpsell,
Sebastian Ertel
Abstract:
Remote attestation (RA) is the foundation for trusted execution environments in the cloud and trusted device driver onboarding in operating systems. However, RA misses a rigorous mechanized definition of its security properties in one of the strongest models, i.e., the semantic model. Such a mechanization requires the concept of State-Separating Proofs (SSP). However, SSP was only recently impleme…
▽ More
Remote attestation (RA) is the foundation for trusted execution environments in the cloud and trusted device driver onboarding in operating systems. However, RA misses a rigorous mechanized definition of its security properties in one of the strongest models, i.e., the semantic model. Such a mechanization requires the concept of State-Separating Proofs (SSP). However, SSP was only recently implemented as a foundational framework in the Rocq Prover. Based on this framework, this paper presents the first mechanized formalization of the fundamental security properties of RA. Our Rocq Prover development first defines digital signatures and formally verifies security against forgery in the strong existential attack model. Based on these results, we define RA and reduce the security of RA to the security of digital signatures. Our development provides evidence that the RA protocol is secure against forgery. Additionally, we extend our reasoning to the primitives of RA and reduce their security to the security of the primitives of the digital signatures. Finally, we found that proving the security of the primitives for digital signatures was not feasible. This observation contrasts textbook formalizations and sparks a discussion on reasoning about the security of libraries in SSP-based frameworks.
△ Less
Submitted 24 February, 2025;
originally announced February 2025.
-
Collisional study of Hilda and quasi-Hilda asteroids
Authors:
P. S. Zain,
R. P. Di Sisto,
R. Gil-Hutton
Abstract:
The Hilda asteroids are located in the outer main belt in a stable 3:2 mean-motion resonance with Jupiter, while the quasi-Hildas (qH) have similar orbits but are not directly under the effect of the MMR. Moreover, cometary activity has been detected in qH. In this study, we investigate the collisional evolution of Hilda asteroids and apply it to study the cratering on asteroid 334 Chicago, as wel…
▽ More
The Hilda asteroids are located in the outer main belt in a stable 3:2 mean-motion resonance with Jupiter, while the quasi-Hildas (qH) have similar orbits but are not directly under the effect of the MMR. Moreover, cometary activity has been detected in qH. In this study, we investigate the collisional evolution of Hilda asteroids and apply it to study the cratering on asteroid 334 Chicago, as well as to determine whether impacts between Hildas and qH can serve as a viable mechanism for inducing cometary activity. We simulated the collisional evolution of Hilda asteroids over a period of 4 Gyr. We considered three initial size-frequency distributions (SFD) and two scaling laws for the collisional outcomes and performed a large set of simulations for each scenario which we used to construct median SFDs of the Hilda population. We also derived impactor SFD on asteroid 334 Chicago and used it to calculate the crater SFD on 334 Chicago. Additionally, we evaluated the subcatastrophic impact timescale between Hilda and qH objects. The observed SFD of Hilda asteroids larger than 3 km is best matched by scenarios assuming that such SFD is mostly primordial, implying minimal collisional activity over time. For smaller sizes, although unconstrained, the SFD steepens significantly due to the catastrophic fragmentation of a small number of multikilometer-sized bodies. We determined that the largest impactor on 334 Chicago measures a few kilometers in size, resulting in a maximum crater size of approximately 30 km. Furthermore, the slope of the crater SFD mirrors that of the initial SFD for subkilometric bodies. While impact events between Hildas and qH can induce observable activity and although stochastic in nature, the timescale of such events exceeds the dynamical lifetime of qH, making them an unlikely primary mechanism for inducing observable activity.
△ Less
Submitted 18 January, 2025;
originally announced January 2025.
-
Study of Baryon number transport using model simulations in $pp$ collisions at LHC Energies
Authors:
M. U. Ashraf,
Junaid Tariq,
Sumaira Ikram,
A. M. Khan,
Jamilla Butt,
Samya Zain
Abstract:
We report on the excitation function of anti-baryon to baryon ratios ($\overline{p}/p$, {\alam /\lam} and {\axi / \xim}) in $pp$ collisions at {\sqrts} = 0.9, 2.76, 7 TeV from DPMJET-III, Pythia~8, EPOS~1.99, and EPOS-LHC model simulations. To study the predictions of these models at {\sqrts} = 13.6 TeV. The anti-baryon to baryon ratios are extremely important for the study of baryon number transp…
▽ More
We report on the excitation function of anti-baryon to baryon ratios ($\overline{p}/p$, {\alam /\lam} and {\axi / \xim}) in $pp$ collisions at {\sqrts} = 0.9, 2.76, 7 TeV from DPMJET-III, Pythia~8, EPOS~1.99, and EPOS-LHC model simulations. To study the predictions of these models at {\sqrts} = 13.6 TeV. The anti-baryon to baryon ratios are extremely important for the study of baryon number transport mechanisms. These ratios help determine the carriers of the baryon number and in the extraction of baryon structure information. Even though all models show a good agreement between model simulations and data, the ratios extracted from DPMJET-III model closely describes data at all energies. It is observed that these ratios converge to unity for various model predictions. This convergence also indicates that the anti-baryon to baryon ratios follow the mass hierarchy, such that the hyperon specie containing more strange quarks ({\alam /\lam} and {\axi / \xim}) approaches unity faster than specie containing fewer strange quarks ($\overline{p}/p$). It is also observed that the $\overline{B}/B$ ratio approaches unity more rapidly with the increase in {\sqrts} energy. At lower energies we observe an excess production of baryons over anti-baryons. However, this effect vanishes at higher energies due to the baryon-anti-baryon pair production and the baryon-anti-baryon yield becomes equal. Using model simulations, we additionally compute the asymmetry, ($A\equiv\frac{N_{p}-N_{\bar{p}}}N_{p}+N_{\bar{p}}}$) for protons. The asymmetry shows a decreasing trend with increase in energy from 0.9 to 7 TeV for all energies. This asymmetry trend is confirmed by model predictions at {\sqrts} = 13.6 TeV which will help to put possible constraints on model calculations at {\sqrts} = 13.6 TeV once the Run-III data for LHC becomes available.
△ Less
Submitted 22 March, 2023; v1 submitted 28 August, 2022;
originally announced August 2022.
-
A mathematical modelling portrait of Wnt signalling in early vertebrate embryogenesis
Authors:
Claudiu V. Giuraniuc,
Shabana Zain,
Shahmama Ghafoor,
Stefan Hoppler
Abstract:
There are two phases of Wnt signalling in early vertebrate embryogenesis: very early, maternal Wnt signalling promotes dorsal development, and slightly later, zygotic Wnt signalling promotes ventral and lateral mesoderm induction. However, recent molecular biology analysis has revealed more complexity among the direct Wnt target genes, with at least five classes. Here in order to test the logic an…
▽ More
There are two phases of Wnt signalling in early vertebrate embryogenesis: very early, maternal Wnt signalling promotes dorsal development, and slightly later, zygotic Wnt signalling promotes ventral and lateral mesoderm induction. However, recent molecular biology analysis has revealed more complexity among the direct Wnt target genes, with at least five classes. Here in order to test the logic and the dynamics of a new Gene Regulatory Network model suggested by these discoveries we use mathematical modelling based on ordinary differential equations (ODEs). Our mathematical modelling of this Gene Regulatory Network reveals that a simplified model, with one "super-gene" for each class is sufficient to a large extent to describe the regulatory behaviour previously observed experimentally.
△ Less
Submitted 1 July, 2022; v1 submitted 1 March, 2022;
originally announced March 2022.
-
New multi-part collisional model of the main belt: The contribution to near-Earth asteroids
Authors:
P. S. Zain,
G. C. de Elía,
R. P. Di Sisto
Abstract:
Aims. We developed a six-part collisional evolution model of the main asteroid belt (MB) and used it to study the contribution of the different regions of the MB to the near-earth asteroids (NEAs). Methods. We built a statistical code called ACDC that simulates the collisional evolution of the MB split into six regions (namely Inner, Middle, Pristine, Outer, Cybele and High-Inclination belts) acco…
▽ More
Aims. We developed a six-part collisional evolution model of the main asteroid belt (MB) and used it to study the contribution of the different regions of the MB to the near-earth asteroids (NEAs). Methods. We built a statistical code called ACDC that simulates the collisional evolution of the MB split into six regions (namely Inner, Middle, Pristine, Outer, Cybele and High-Inclination belts) according to the positions of the major resonances present there ($ν_{6}$, 3:1J, 5:2J, 7:3J and 2:1J). We consider the Yarkovsky effect and the mentioned resonances as the main mechanism that removes asteroids from the different regions of the MB and delivers them to the NEA region. We calculated the evolution of the NEAs coming from the different source regions by considering the bodies delivered by the resonances and mean dynamical timescales in the NEA population. Results. Our model is in agreement with the major observational constraints associated with the MB, such as the size distributions of the different regions of the MB and the number of large asteroid families. It is also able to reproduce the observed NEAs with H < 16 and agrees with recent estimations for H < 20, but deviates for smaller sizes. We find that most sources make a significant contribution to the NEAs; however the Inner and Middle belts stand out as the most important source of NEAs followed by the Outer belt. The contributions of the Pristine and Cybele regions are minor. The High-Inclination belt is the source of only a fraction of the actual observed NEAs with high inclination, as there are dynamical processes in that region that enable asteroids to increase and decrease their inclinations.
△ Less
Submitted 26 May, 2020;
originally announced May 2020.
-
Planetary formation and water delivery in the habitable zone around solar-type stars in different dynamical environments
Authors:
Patricio Salvador Zain,
Gonzalo Carlos de Elía,
María Paula Ronco,
Octavio Miguel Guilera
Abstract:
Aims. We study the formation and water delivery of planets in the habitable zone (HZ) around solar-type stars. In particular, we study different dynamical environments that are defined by the most massive body in the system. Methods. First of all, a semi-analytical model was used to define the mass of the protoplanetary disks that produce each of the five dynamical scenarios of our research. Then,…
▽ More
Aims. We study the formation and water delivery of planets in the habitable zone (HZ) around solar-type stars. In particular, we study different dynamical environments that are defined by the most massive body in the system. Methods. First of all, a semi-analytical model was used to define the mass of the protoplanetary disks that produce each of the five dynamical scenarios of our research. Then, we made use of the same semi-analytical model to describe the evolution of embryos and planetesimals during the gaseous phase. Finally, we carried out N-body simulations of planetary accretion in order to analyze the formation and water delivery of planets in the HZ in the different dynamical environments. Results. Water worlds are efficiently formed in the HZ in different dynamical scenarios. In systems with a giant planet analog to Jupiter or Saturn around the snow line, super-Earths tend to migrate into the HZ from outside the snow line as a result of interactions with other embryos and accrete water only during the gaseous phase. In systems without giant planets, Earths and super-Earths with high water by mass contents can either be formed in situ in the HZ or migrate into it from outer regions, and water can be accreted during the gaseous phase and in collisions with water-rich embryos and planetesimals. Conclusions. The formation of planets in the HZ with very high water by mass contents seems to be a common process around Sun- like stars. Our research suggests that such planets are still very efficiently produced in different dynamical environments. Moreover, our study indicates that the formation of planets in the HZ with masses and water contents similar to those of Earth seems to be a rare process around solar-type stars in the systems under consideration.
△ Less
Submitted 12 October, 2017;
originally announced October 2017.
-
The Physics of the B Factories
Authors:
A. J. Bevan,
B. Golob,
Th. Mannel,
S. Prell,
B. D. Yabsley,
K. Abe,
H. Aihara,
F. Anulli,
N. Arnaud,
T. Aushev,
M. Beneke,
J. Beringer,
F. Bianchi,
I. I. Bigi,
M. Bona,
N. Brambilla,
J. B rodzicka,
P. Chang,
M. J. Charles,
C. H. Cheng,
H. -Y. Cheng,
R. Chistov,
P. Colangelo,
J. P. Coleman,
A. Drutskoy
, et al. (2009 additional authors not shown)
Abstract:
This work is on the Physics of the B Factories. Part A of this book contains a brief description of the SLAC and KEK B Factories as well as their detectors, BaBar and Belle, and data taking related issues. Part B discusses tools and methods used by the experiments in order to obtain results. The results themselves can be found in Part C.
Please note that version 3 on the archive is the auxiliary…
▽ More
This work is on the Physics of the B Factories. Part A of this book contains a brief description of the SLAC and KEK B Factories as well as their detectors, BaBar and Belle, and data taking related issues. Part B discusses tools and methods used by the experiments in order to obtain results. The results themselves can be found in Part C.
Please note that version 3 on the archive is the auxiliary version of the Physics of the B Factories book. This uses the notation alpha, beta, gamma for the angles of the Unitarity Triangle. The nominal version uses the notation phi_1, phi_2 and phi_3. Please cite this work as Eur. Phys. J. C74 (2014) 3026.
△ Less
Submitted 31 October, 2015; v1 submitted 24 June, 2014;
originally announced June 2014.
